Additional Proof Generation Information

The Proof Call

\(Prove[
        Theorem["Root Irrational"], 
using -> {Definition["Rational"], Lemma["Coprime for Two"], 
            Lemma["Multiply Root Equation"], Lemma["Euclid"], 
            Definition["Divisible"], Lemma["Simplify by Cancelling"], 
            Lemma["Squares Preserve Naturals"]}, 
by -> PredicateProver, SearchDepth -> ∞] // 
      Timing\)

Version Info

THEOREMA Version: 1.1α1

License Number: D11A-00017

Expiration Date: 2001/12/31

Theorema`: Revision: 1.5 , Date: 2001/04/10 13:57:13 , Last modified by: marcus

Theorema`Evaluators`Common`SessionHandling`: Revision: 1.5 , Date: 2000/07/21 10:15:47 , Last modified by: wwindste

Theorema`Evaluators`ComputationalSession`: Revision: 1.23 , Date: 2001/03/23 08:52:57 , Last modified by: wwindste

Theorema`General`Auxiliary`: Revision: 1.29 , Date: 2001/03/14 14:37:23 , Last modified by: marcus

Theorema`General`LookupTable`: Revision: 1.10 , Date: 1999/12/03 15:52:48 , Last modified by: fpiroi

Theorema`General`TmaException`: Revision: 1.4 , Date: 1999/12/03 15:52:48 , Last modified by: fpiroi

Theorema`Language`General`HandleFormulae`: Revision: 1.51 , Date: 2001/01/15 16:00:55 , Last modified by: wwindste

Theorema`Language`Semantics`Container`: Revision: 1.9 , Date: 2000/09/19 14:31:32 , Last modified by: wwindste

Theorema`Language`Semantics`FormalText`: Revision: 1.6 , Date: 2000/02/09 12:04:10 , Last modified by: wwindste

Theorema`Language`Semantics`UserLanguage`: Revision: 1.63 , Date: 2001/08/30 14:05:09 , Last modified by: wwindste

Theorema`Language`Syntax`Connective`: Revision: 1.9 , Date: 1999/07/02 13:34:00 , Last modified by: wwindste

Theorema`Language`Syntax`Container`: Revision: 1.24 , Date: 1999/05/27 15:45:19 , Last modified by: wwindste

Theorema`Language`Syntax`Core`: Revision: 1.84 , Date: 2001/08/30 13:59:45 , Last modified by: tkutsia

Theorema`Language`Syntax`Domain`: Revision: 1.1 , Date: 1999/06/18 13:12:07 , Last modified by: wwindste

Theorema`Language`Syntax`FormalText`: Revision: 1.11 , Date: 2000/07/20 13:24:45 , Last modified by: wwindste

Theorema`Language`Syntax`Functor`: Revision: 1.15 , Date: 2000/02/18 15:13:01 , Last modified by: wwindste

Theorema`Language`Syntax`Number`: Revision: 1.23 , Date: 1999/08/13 01:53:07 , Last modified by: kriftner

Theorema`Language`Syntax`Operator`: Revision: 1.19 , Date: 2001/03/29 08:17:14 , Last modified by: marcus

Theorema`Language`Syntax`Parser`: Revision: 1.55 , Date: 2001/04/17 06:40:36 , Last modified by: wwindste

Theorema`Language`Syntax`Quantifier`: Revision: 1.33 , Date: 1999/06/23 09:15:51 , Last modified by: kriftner

Theorema`Language`Syntax`Set`: Revision: 1.27 , Date: 2000/08/25 16:43:00 , Last modified by: wwindste

Theorema`Language`Syntax`Tuple`: Revision: 1.19 , Date: 1999/06/18 09:25:18 , Last modified by: wwindste

Theorema`Language`Syntax`UserLanguage`: Revision: 1.31 , Date: 2000/08/09 13:56:28 , Last modified by: wwindste

Theorema`Provers`Common`BasicProofCells`: Revision: 1.26 , Date: 2001/03/23 09:31:45 , Last modified by: wwindste

Theorema`Provers`Common`ConstraintLanguage`: Revision: 1.9 , Date: 1999/09/30 11:27:14 , Last modified by: dvasaru

Theorema`Provers`Common`HandleFormulae`: Revision: 1.36 , Date: 2001/05/22 09:33:11 , Last modified by: wwindste

Theorema`Provers`Common`Header`English`: Revision: 1.20 , Date: 2001/05/10 07:09:50 , Last modified by: fpiroi

Theorema`Provers`Common`Keywords`: Revision: 1.8 , Date: 2001/05/10 07:09:25 , Last modified by: fpiroi

Theorema`Provers`Common`ProofCells`: Revision: 1.40 , Date: 2001/02/08 09:04:02 , Last modified by: wwindste

Theorema`Provers`Common`ProofObject`: Revision: 1.29 , Date: 2001/05/09 13:19:00 , Last modified by: fpiroi

Theorema`Provers`Common`ProofObjectInterface`: Revision: 1.14 , Date: 2000/08/02 09:03:58 , Last modified by: tjebelea

Theorema`Provers`Common`ProofObjectManagement`: Revision: 1.47 , Date: 2001/01/04 13:07:19 , Last modified by: wwindste

Theorema`Provers`PLM`HandleConstraints`: Revision: 1.1 , Date: 2000/05/24 12:55:09 , Last modified by: bkonev

Theorema`Provers`PLM`MetaUnification`: Revision: 1.1 , Date: 2000/05/24 12:56:40 , Last modified by: bkonev

Theorema`Provers`PLM`Unification`: Revision: 1.1 , Date: 2000/05/24 14:26:18 , Last modified by: bkonev

Theorema`Provers`PredicateLogic`Auxiliary`: Revision: 1.5 , Date: 1999/07/23 13:28:33 , Last modified by: fpiroi

Theorema`Provers`PredicateLogic`Header`English`: Revision: 1.28 , Date: 1999/07/07 10:50:37 , Last modified by: tjebelea

Theorema`Provers`PredicateLogic`Keywords`: Revision: 1.12 , Date: 2000/03/31 15:40:36 , Last modified by: tjebelea

Theorema`Provers`PredicateLogic`Prover`: Revision: 1.43 , Date: 2001/04/02 14:54:33 , Last modified by: tjebelea

Theorema`Provers`Propositional`Auxiliary`: Revision: 1.9 , Date: 2001/04/02 14:53:25 , Last modified by: tjebelea

Theorema`Provers`Propositional`Header`English`: Revision: 1.7 , Date: 2000/10/06 11:29:40 , Last modified by: fpiroi

Theorema`Provers`Propositional`Keywords`: Revision: 1.5 , Date: 2000/10/06 12:52:45 , Last modified by: fpiroi

Theorema`Provers`UserProvers`PredicateProver`: Revision: 1.13 , Date: 2001/04/02 14:52:15 , Last modified by: tjebelea

Theorema`System`Debug`: Revision: 1.8 , Date: 1999/01/14 15:24:33 , Last modified by: wwindste

Theorema`System`Toolbox`: Revision: ?, Date: ?, Last modified by: ?

Theorema`System`Trace`: Revision: 1.16 , Date: 2001/02/06 12:12:48 , Last modified by: wwindste

Theorema`User`Preferences`: Revision: 1.4 , Date: 2000/02/28 14:02:34 , Last modified by: wwindste

Utilities`FilterOptions`: Revision: ?, Date: ?, Last modified by: ?

Formulae Occuring during the Proof

(1)rat[(Sqrt[p])]

(10)nat[(((Subscript[m, 0]))^2)]

(100)(Underscript[∀, d ])(nat[d]=>((((((((Subscript[m, 0]))^2)))^2)=p*d)=>p∣((((((Subscript[m, 0]))^2)))^2)))

(101)p∣((((((Subscript[m, 0]))^2)))^2)=>(Underscript[∃, d ])(nat[d]∧(((((((Subscript[m, 0]))^2)))^2)=p*d))

(102)nat[(((((((((Subscript[m, 0]))^2)))^2)))^2)]

(103)(((((((Subscript[n, 0]))^2)))^2)⊥(((Subscript[m, 0]))^2))=>p∤((((((Subscript[n, 0]))^2)))^2)

(104)(((Subscript[n, 0]))^2)≠p*((((((Subscript[n, 0]))^2)))^2)

(105)(((((((Subscript[n, 0]))^2)))^2)⊥(Subscript[m, 0]))=>p∤((((((Subscript[n, 0]))^2)))^2)

(106)(Subscript[n, 0])≠p*((((((Subscript[n, 0]))^2)))^2)

(107)(Underscript[∀, m ])(nat[m]=>((m⊥((((((Subscript[n, 0]))^2)))^2))=>¬(p∣((((((Subscript[n, 0]))^2)))^2)∧p∣m)))

(108)p∣(((((((((Subscript[n, 0]))^2)))^2)))^2)=>p∣((((((Subscript[n, 0]))^2)))^2)

(109)(Underscript[∀, d ])(nat[d]=>((((((((Subscript[n, 0]))^2)))^2)=p*d)=>p∣((((((Subscript[n, 0]))^2)))^2)))

(11)(Underscript[∀, m ])(nat[m]=>((m⊥(Subscript[n, 0]))=>¬(p∣(Subscript[n, 0])∧p∣m)))

(110)p∣((((((Subscript[n, 0]))^2)))^2)=>(Underscript[∃, d ])(nat[d]∧(((((((Subscript[n, 0]))^2)))^2)=p*d))

(111)nat[(((((((((Subscript[n, 0]))^2)))^2)))^2)]

(112)((((Subscript[m, 0]))^2)⊥(((Subscript[m, 0]))^2))=>p∤(((Subscript[m, 0]))^2)

(113)(((Subscript[n, 0]))^2)≠p*(((Subscript[m, 0]))^2)

(114)((((Subscript[m, 0]))^2)⊥(Subscript[m, 0]))=>p∤(((Subscript[m, 0]))^2)

(115)(Subscript[n, 0])≠p*(((Subscript[m, 0]))^2)

(116)((((Subscript[n, 0]))^2)⊥(((Subscript[m, 0]))^2))=>p∤(((Subscript[n, 0]))^2)

(117)(((Subscript[n, 0]))^2)≠p*(((Subscript[n, 0]))^2)

(118)((((Subscript[n, 0]))^2)⊥(Subscript[m, 0]))=>p∤(((Subscript[n, 0]))^2)

(119)(Subscript[n, 0])≠p*(((Subscript[n, 0]))^2)

(12)p∣(((Subscript[n, 0]))^2)=>p∣(Subscript[n, 0])

(120)((Subscript[m, 0])⊥(((Subscript[m, 0]))^2))=>p∤(Subscript[m, 0])

(121)(((Subscript[n, 0]))^2)≠p*(Subscript[m, 0])

(122)((Subscript[m, 0])⊥(Subscript[m, 0]))=>p∤(Subscript[m, 0])

(123)(Subscript[n, 0])≠p*(Subscript[m, 0])

(124)((Subscript[n, 0])⊥(((Subscript[m, 0]))^2))=>p∤(Subscript[n, 0])

(125)(((Subscript[n, 0]))^2)≠p*(Subscript[n, 0])

(126)((Subscript[n, 0])⊥(Subscript[m, 0]))=>p∤(Subscript[n, 0])

(127)(Subscript[n, 0])≠p*(Subscript[n, 0])

(128)nat[(((Subscript[m, 0]))^2)]=>¬((((Subscript[m, 0]))^2)⊥(((Subscript[m, 0]))^2))

(129)nat[(((Subscript[m, 0]))^2)]=>¬((((Subscript[m, 0]))^2)⊥(Subscript[m, 0]))

(13)(Underscript[∀, d ])(nat[d]=>(((Subscript[n, 0])=p*d)=>p∣(Subscript[n, 0])))

(130)(Underscript[∀, m ])(nat[(((Subscript[m, 0]))^2)]∧nat[m]=>((m⊥(((Subscript[m, 0]))^2))=>p∤m))

(131)nat[(Subscript[m, 0])]=>p∣(Subscript[m, 0])

(132)nat[(((Subscript[m, 0]))^2)]=>(Underscript[∃, d ])(nat[d]∧((((Subscript[m, 0]))^2)=p*d))

(133)nat[(Subscript[m, 0])]=>¬((Subscript[m, 0])⊥(((Subscript[m, 0]))^2))

(134)nat[(Subscript[m, 0])]=>¬((Subscript[m, 0])⊥(Subscript[m, 0]))

(135)(Underscript[∀, m ])(nat[(Subscript[m, 0])]∧nat[m]=>((m⊥(Subscript[m, 0]))=>p∤m))

(136)nat[(Subscript[m, 0])]=>(Underscript[∃, d ])(nat[d]∧((Subscript[m, 0])=p*d))

(137)nat[(Subscript[n, 0])]=>p∤(((Subscript[n, 0]))^2)

(138)(Underscript[∀, d ])(nat[(Subscript[n, 0])]∧nat[d]=>(Subscript[n, 0])≠p*d)

(139)nat[(((Subscript[n, 0]))^2)]=>p∤((((((Subscript[n, 0]))^2)))^2)

(14)p∣(Subscript[n, 0])=>(Underscript[∃, d ])(nat[d]∧((Subscript[n, 0])=p*d))

(140)(Underscript[∀, d ])(nat[(((Subscript[n, 0]))^2)]∧nat[d]=>(((Subscript[n, 0]))^2)≠p*d)

(141)nat[((((((Subscript[n, 0]))^2)))^2)]=>p∤(((((((((Subscript[n, 0]))^2)))^2)))^2)

(142)(Underscript[∀, d ])(nat[((((((Subscript[n, 0]))^2)))^2)]∧nat[d]=>((((((Subscript[n, 0]))^2)))^2)≠p*d)

(143)p∤(((((((((Subscript[n, 0]))^2)))^2)))^2)

(144)¬((((Subscript[m, 0]))^2)⊥(((Subscript[m, 0]))^2))

(145)(Underscript[∃, d ])(nat[d]∧((((Subscript[m, 0]))^2)=p*d))

(146)¬((Subscript[m, 0])⊥(((Subscript[m, 0]))^2))

(147)(Underscript[∃, d ])(nat[d]∧((Subscript[m, 0])=p*d))

(148)nat[(Subscript[d, 2])]∧((((Subscript[m, 0]))^2)=p*(Subscript[d, 2]))

(148.1)nat[(Subscript[d, 2])]

(148.2)(((Subscript[m, 0]))^2)=p*(Subscript[d, 2])

(149)nat[(Subscript[d, 3])]∧((Subscript[m, 0])=p*(Subscript[d, 3]))

(149.1)nat[(Subscript[d, 3])]

(149.2)(Subscript[m, 0])=p*(Subscript[d, 3])

(15)nat[(((Subscript[n, 0]))^2)]

(150)(Underscript[∀, d ])(nat[d]=>((((((Subscript[n, 0]))^2)))^2)≠p*d)

(151)(Underscript[∀, d ])(nat[d]=>(Subscript[n, 0])≠p*d)

(152)(Underscript[∀, m ])(nat[m]=>((m⊥(Subscript[m, 0]))=>p∤m))

(153)(Underscript[∀, d ])(nat[d]=>(((Subscript[n, 0]))^2)≠p*d)

(154)(Underscript[∀, m ])(nat[m]=>((m⊥(((Subscript[m, 0]))^2))=>p∤m))

(155)(Underscript[∀, d ])(nat[d]=>((((((Subscript[n, 0]))^2)))^2)≠p*d)

(156)nat[(Subscript[m, 0])]=>(((Subscript[m, 0])⊥((((((Subscript[m, 0]))^2)))^2))=>p∤((((((Subscript[m, 0]))^2)))^2))

(157)nat[(Subscript[m, 0])]=>(((Subscript[m, 0])⊥(Subscript[d, 0]))=>p∤(Subscript[d, 0]))

(158)nat[(Subscript[m, 0])]=>(((Subscript[m, 0])⊥(Subscript[d, 1]))=>p∤(Subscript[d, 1]))

(159)nat[(((Subscript[m, 0]))^2)]=>(((((Subscript[m, 0]))^2)⊥((((((Subscript[m, 0]))^2)))^2))=>p∤((((((Subscript[m, 0]))^2)))^2))

(16)nat[(Subscript[m, 0])]=>¬(p∣(Subscript[n, 0])∧p∣(Subscript[m, 0]))

(160)nat[(((Subscript[m, 0]))^2)]=>(((((Subscript[m, 0]))^2)⊥(Subscript[d, 0]))=>p∤(Subscript[d, 0]))

(161)nat[(((Subscript[m, 0]))^2)]=>(((((Subscript[m, 0]))^2)⊥(Subscript[d, 1]))=>p∤(Subscript[d, 1]))

(162)((((((Subscript[n, 0]))^2)))^2)≠p*(Subscript[n, 0])

(163)(((((((Subscript[m, 0]))^2)))^2)=p*(Subscript[n, 0]))=>p∣((((((Subscript[m, 0]))^2)))^2)

(164)((Subscript[n, 0])⊥((((((Subscript[m, 0]))^2)))^2))=>¬(p∣((((((Subscript[m, 0]))^2)))^2)∧p∣(Subscript[n, 0]))

(165)((Subscript[d, 0])=p*(Subscript[n, 0]))=>p∣(Subscript[d, 0])

(166)((Subscript[n, 0])⊥(Subscript[d, 0]))=>¬(p∣(Subscript[d, 0])∧p∣(Subscript[n, 0]))

(167)((Subscript[d, 1])=p*(Subscript[n, 0]))=>p∣(Subscript[d, 1])

(168)((Subscript[n, 0])⊥(Subscript[d, 1]))=>¬(p∣(Subscript[d, 1])∧p∣(Subscript[n, 0]))

(169)((((((Subscript[n, 0]))^2)))^2)≠p*(Subscript[m, 0])

(17)¬(p∣(Subscript[n, 0])∧p∣(Subscript[m, 0]))

(170)(((((((Subscript[m, 0]))^2)))^2)=p*(Subscript[m, 0]))=>p∣((((((Subscript[m, 0]))^2)))^2)

(171)((Subscript[m, 0])⊥((((((Subscript[m, 0]))^2)))^2))=>¬(p∣((((((Subscript[m, 0]))^2)))^2)∧p∣(Subscript[m, 0]))

(172)((Subscript[d, 0])=p*(Subscript[m, 0]))=>p∣(Subscript[d, 0])

(173)((Subscript[m, 0])⊥(Subscript[d, 0]))=>¬(p∣(Subscript[d, 0])∧p∣(Subscript[m, 0]))

(174)((Subscript[d, 1])=p*(Subscript[m, 0]))=>p∣(Subscript[d, 1])

(175)((Subscript[m, 0])⊥(Subscript[d, 1]))=>¬(p∣(Subscript[d, 1])∧p∣(Subscript[m, 0]))

(176)((((((Subscript[n, 0]))^2)))^2)≠p*(((Subscript[n, 0]))^2)

(177)(((((((Subscript[m, 0]))^2)))^2)=p*(((Subscript[n, 0]))^2))=>p∣((((((Subscript[m, 0]))^2)))^2)

(178)((((Subscript[n, 0]))^2)⊥((((((Subscript[m, 0]))^2)))^2))=>¬(p∣((((((Subscript[m, 0]))^2)))^2)∧p∣(((Subscript[n, 0]))^2))

(179)((Subscript[d, 0])=p*(((Subscript[n, 0]))^2))=>p∣(Subscript[d, 0])

(18)p∤(Subscript[n, 0])∨p∤(Subscript[m, 0])

(180)((((Subscript[n, 0]))^2)⊥(Subscript[d, 0]))=>¬(p∣(Subscript[d, 0])∧p∣(((Subscript[n, 0]))^2))

(181)((Subscript[d, 1])=p*(((Subscript[n, 0]))^2))=>p∣(Subscript[d, 1])

(182)((((Subscript[n, 0]))^2)⊥(Subscript[d, 1]))=>¬(p∣(Subscript[d, 1])∧p∣(((Subscript[n, 0]))^2))

(183)((((((Subscript[n, 0]))^2)))^2)≠p*(((Subscript[m, 0]))^2)

(184)(((((((Subscript[m, 0]))^2)))^2)=p*(((Subscript[m, 0]))^2))=>p∣((((((Subscript[m, 0]))^2)))^2)

(185)((((Subscript[m, 0]))^2)⊥((((((Subscript[m, 0]))^2)))^2))=>¬(p∣((((((Subscript[m, 0]))^2)))^2)∧p∣(((Subscript[m, 0]))^2))

(186)((Subscript[d, 0])=p*(((Subscript[m, 0]))^2))=>p∣(Subscript[d, 0])

(187)((((Subscript[m, 0]))^2)⊥(Subscript[d, 0]))=>¬(p∣(Subscript[d, 0])∧p∣(((Subscript[m, 0]))^2))

(188)((Subscript[d, 1])=p*(((Subscript[m, 0]))^2))=>p∣(Subscript[d, 1])

(189)((((Subscript[m, 0]))^2)⊥(Subscript[d, 1]))=>¬(p∣(Subscript[d, 1])∧p∣(((Subscript[m, 0]))^2))

(19)nat[(((Subscript[m, 0]))^2)]∧nat[(((Subscript[n, 0]))^2)]=>p∣(((Subscript[m, 0]))^2)

(190)(((Subscript[n, 0]))^2)=p*(((Subscript[d, 0]))^2)

(191)((((((Subscript[n, 0]))^2)))^2)≠p*((((((Subscript[n, 0]))^2)))^2)

(192)(((((((Subscript[m, 0]))^2)))^2)=p*((((((Subscript[n, 0]))^2)))^2))=>p∣((((((Subscript[m, 0]))^2)))^2)

(193)(((((((Subscript[n, 0]))^2)))^2)⊥((((((Subscript[m, 0]))^2)))^2))=>¬(p∣((((((Subscript[m, 0]))^2)))^2)∧p∣((((((Subscript[n, 0]))^2)))^2))

(194)((Subscript[d, 0])=p*((((((Subscript[n, 0]))^2)))^2))=>p∣(Subscript[d, 0])

(195)(((((((Subscript[n, 0]))^2)))^2)⊥(Subscript[d, 0]))=>¬(p∣(Subscript[d, 0])∧p∣((((((Subscript[n, 0]))^2)))^2))

(196)((Subscript[d, 1])=p*((((((Subscript[n, 0]))^2)))^2))=>p∣(Subscript[d, 1])

(197)(((((((Subscript[n, 0]))^2)))^2)⊥(Subscript[d, 1]))=>¬(p∣(Subscript[d, 1])∧p∣((((((Subscript[n, 0]))^2)))^2))

(198)((((((Subscript[n, 0]))^2)))^2)≠p*((((((Subscript[m, 0]))^2)))^2)

(199)(((((((Subscript[m, 0]))^2)))^2)=p*((((((Subscript[m, 0]))^2)))^2))=>p∣((((((Subscript[m, 0]))^2)))^2)

(2)(Underscript[∃, m,n])((nat[n]∧nat[m])∧((((Sqrt[p]))=(m/n))∧(m⊥n)))

(20)(Underscript[∀, k ])(((Subscript[m, 0])=p*k)=>((((Subscript[n, 0]))^2)=p*(k^2)))

(200)(((((((Subscript[m, 0]))^2)))^2)⊥((((((Subscript[m, 0]))^2)))^2))=>¬(p∣((((((Subscript[m, 0]))^2)))^2)∧p∣((((((Subscript[m, 0]))^2)))^2))

(201)((Subscript[d, 0])=p*((((((Subscript[m, 0]))^2)))^2))=>p∣(Subscript[d, 0])

(202)(((((((Subscript[m, 0]))^2)))^2)⊥(Subscript[d, 0]))=>¬(p∣(Subscript[d, 0])∧p∣((((((Subscript[m, 0]))^2)))^2))

(203)((Subscript[d, 1])=p*((((((Subscript[m, 0]))^2)))^2))=>p∣(Subscript[d, 1])

(204)(((((((Subscript[m, 0]))^2)))^2)⊥(Subscript[d, 1]))=>¬(p∣(Subscript[d, 1])∧p∣((((((Subscript[m, 0]))^2)))^2))

(205)((((((Subscript[n, 0]))^2)))^2)≠p*(Subscript[d, 0])

(206)(((((((Subscript[m, 0]))^2)))^2)=p*(Subscript[d, 0]))=>p∣((((((Subscript[m, 0]))^2)))^2)

(207)((Subscript[d, 0])⊥((((((Subscript[m, 0]))^2)))^2))=>¬(p∣((((((Subscript[m, 0]))^2)))^2)∧p∣(Subscript[d, 0]))

(208)((Subscript[d, 0])=p*(Subscript[d, 0]))=>p∣(Subscript[d, 0])

(209)((Subscript[d, 0])⊥(Subscript[d, 0]))=>¬(p∣(Subscript[d, 0])∧p∣(Subscript[d, 0]))

(21)((((Subscript[m, 0]))^2)⊥(Subscript[m, 0]))=>¬(p∣(Subscript[m, 0])∧p∣(((Subscript[m, 0]))^2))

(210)((Subscript[d, 1])=p*(Subscript[d, 0]))=>p∣(Subscript[d, 1])

(211)((Subscript[d, 0])⊥(Subscript[d, 1]))=>¬(p∣(Subscript[d, 1])∧p∣(Subscript[d, 0]))

(212)((((((Subscript[n, 0]))^2)))^2)≠p*(Subscript[d, 1])

(213)(((((((Subscript[m, 0]))^2)))^2)=p*(Subscript[d, 1]))=>p∣((((((Subscript[m, 0]))^2)))^2)

(214)((Subscript[d, 1])⊥((((((Subscript[m, 0]))^2)))^2))=>¬(p∣((((((Subscript[m, 0]))^2)))^2)∧p∣(Subscript[d, 1]))

(215)((Subscript[d, 0])=p*(Subscript[d, 1]))=>p∣(Subscript[d, 0])

(216)((Subscript[d, 1])⊥(Subscript[d, 0]))=>¬(p∣(Subscript[d, 0])∧p∣(Subscript[d, 1]))

(217)((Subscript[d, 1])=p*(Subscript[d, 1]))=>p∣(Subscript[d, 1])

(218)((Subscript[d, 1])⊥(Subscript[d, 1]))=>¬(p∣(Subscript[d, 1])∧p∣(Subscript[d, 1]))

(219)(Underscript[∀, d ])(nat[(((((((((Subscript[n, 0]))^2)))^2)))^2)]∧nat[d]=>(((((((((Subscript[n, 0]))^2)))^2)))^2)≠p*d)

(22)((Subscript[m, 0])=p*(((Subscript[m, 0]))^2))=>p∣(Subscript[m, 0])

(220)nat[(((((((((Subscript[n, 0]))^2)))^2)))^2)]=>p∤((((((((((((Subscript[n, 0]))^2)))^2)))^2)))^2)

(221)(Underscript[∀, n ])(((((Subscript[m, 0]))^2)=p*(n^2))=>((n^2)=p*(((Subscript[d, 3]))^2)))

(222)nat[(Subscript[m, 0])]∧nat[(Subscript[d, 3])]=>p∣(Subscript[m, 0])

(223)(((Subscript[n, 0]))^2)=p*(((Subscript[d, 3]))^2)

(224)nat[(((Subscript[d, 3]))^2)]

(225)p∣(Subscript[d, 3])=>(Underscript[∃, d ])(nat[d]∧((Subscript[d, 3])=p*d))

(226)(Underscript[∀, d ])(nat[d]=>(((Subscript[d, 3])=p*d)=>p∣(Subscript[d, 3])))

(227)p∣(((Subscript[d, 3]))^2)=>p∣(Subscript[d, 3])

(228)(Underscript[∀, m ])(nat[m]=>((m⊥(Subscript[d, 3]))=>¬(p∣(Subscript[d, 3])∧p∣m)))

(229)(Subscript[n, 0])≠p*(Subscript[d, 3])

(23)((((Subscript[m, 0]))^2)⊥(Subscript[n, 0]))=>¬(p∣(Subscript[n, 0])∧p∣(((Subscript[m, 0]))^2))

(230)((Subscript[d, 3])⊥(Subscript[m, 0]))=>p∤(Subscript[d, 3])

(231)(((Subscript[n, 0]))^2)≠p*(Subscript[d, 3])

(232)((Subscript[d, 3])⊥(((Subscript[m, 0]))^2))=>p∤(Subscript[d, 3])

(233)((((((Subscript[n, 0]))^2)))^2)≠p*(Subscript[d, 3])

(234)(((((((Subscript[m, 0]))^2)))^2)=p*(Subscript[d, 3]))=>p∣((((((Subscript[m, 0]))^2)))^2)

(235)((Subscript[d, 3])⊥((((((Subscript[m, 0]))^2)))^2))=>¬(p∣((((((Subscript[m, 0]))^2)))^2)∧p∣(Subscript[d, 3]))

(236)((Subscript[d, 0])=p*(Subscript[d, 3]))=>p∣(Subscript[d, 0])

(237)((Subscript[d, 3])⊥(Subscript[d, 0]))=>¬(p∣(Subscript[d, 0])∧p∣(Subscript[d, 3]))

(238)((Subscript[d, 1])=p*(Subscript[d, 3]))=>p∣(Subscript[d, 1])

(239)((Subscript[d, 3])⊥(Subscript[d, 1]))=>¬(p∣(Subscript[d, 1])∧p∣(Subscript[d, 3]))

(24)((Subscript[n, 0])=p*(((Subscript[m, 0]))^2))=>p∣(Subscript[n, 0])

(240)(Underscript[∀, n ])((((((((Subscript[m, 0]))^2)))^2)=p*(n^2))=>((n^2)=p*(((Subscript[d, 2]))^2)))

(241)nat[(((Subscript[m, 0]))^2)]∧nat[(Subscript[d, 2])]=>p∣(((Subscript[m, 0]))^2)

(242)nat[(((Subscript[d, 2]))^2)]

(243)p∣(Subscript[d, 2])=>(Underscript[∃, d ])(nat[d]∧((Subscript[d, 2])=p*d))

(244)(Underscript[∀, d ])(nat[d]=>(((Subscript[d, 2])=p*d)=>p∣(Subscript[d, 2])))

(245)p∣(((Subscript[d, 2]))^2)=>p∣(Subscript[d, 2])

(246)(Underscript[∀, m ])(nat[m]=>((m⊥(Subscript[d, 2]))=>¬(p∣(Subscript[d, 2])∧p∣m)))

(247)(Subscript[n, 0])≠p*(Subscript[d, 2])

(248)((Subscript[d, 2])⊥(Subscript[m, 0]))=>p∤(Subscript[d, 2])

(249)(((Subscript[n, 0]))^2)≠p*(Subscript[d, 2])

(25)(Underscript[∀, m ])(nat[m]=>((m⊥(((Subscript[m, 0]))^2))=>¬(p∣(((Subscript[m, 0]))^2)∧p∣m)))

(250)((Subscript[d, 2])⊥(((Subscript[m, 0]))^2))=>p∤(Subscript[d, 2])

(251)((((((Subscript[n, 0]))^2)))^2)≠p*(Subscript[d, 2])

(252)(((((((Subscript[m, 0]))^2)))^2)=p*(Subscript[d, 2]))=>p∣((((((Subscript[m, 0]))^2)))^2)

(253)((Subscript[d, 2])⊥((((((Subscript[m, 0]))^2)))^2))=>¬(p∣((((((Subscript[m, 0]))^2)))^2)∧p∣(Subscript[d, 2]))

(254)((Subscript[d, 0])=p*(Subscript[d, 2]))=>p∣(Subscript[d, 0])

(255)((Subscript[d, 2])⊥(Subscript[d, 0]))=>¬(p∣(Subscript[d, 0])∧p∣(Subscript[d, 2]))

(256)((Subscript[d, 1])=p*(Subscript[d, 2]))=>p∣(Subscript[d, 1])

(257)((Subscript[d, 2])⊥(Subscript[d, 1]))=>¬(p∣(Subscript[d, 1])∧p∣(Subscript[d, 2]))

(258)(Underscript[∀, m ])(¬(((m^2)=p*(((Subscript[n, 0]))^2))∧(m=p*(Subscript[n, 0]))))

(259)((Sqrt[p]))≠(((Subscript[n, 0]))/((Subscript[n, 0])))

(26)p∣((((((Subscript[m, 0]))^2)))^2)=>p∣(((Subscript[m, 0]))^2)

(260)(Subscript[m, 0])≠p*(Subscript[n, 0])

(261)(Underscript[∀, m ])(¬(((m^2)=p*(((Subscript[n, 0]))^2))∧(m=p*(Subscript[m, 0]))))

(262)((Sqrt[p]))≠(((Subscript[n, 0]))/((Subscript[m, 0])))

(263)(Subscript[m, 0])≠p*(Subscript[m, 0])

(264)nat[((((((((((((Subscript[n, 0]))^2)))^2)))^2)))^2)]

(265)p∣(((((((((Subscript[n, 0]))^2)))^2)))^2)=>(Underscript[∃, d ])(nat[d]∧((((((((((Subscript[n, 0]))^2)))^2)))^2)=p*d))

(266)(Underscript[∀, d ])(nat[d]=>(((((((((((Subscript[n, 0]))^2)))^2)))^2)=p*d)=>p∣(((((((((Subscript[n, 0]))^2)))^2)))^2)))

(267)p∣((((((((((((Subscript[n, 0]))^2)))^2)))^2)))^2)=>p∣(((((((((Subscript[n, 0]))^2)))^2)))^2)

(268)(Underscript[∀, m ])(nat[m]=>((m⊥(((((((((Subscript[n, 0]))^2)))^2)))^2))=>¬(p∣(((((((((Subscript[n, 0]))^2)))^2)))^2)∧p∣m)))

(269)(Subscript[n, 0])≠p*(((((((((Subscript[n, 0]))^2)))^2)))^2)

(27)(Underscript[∀, d ])(nat[d]=>(((((Subscript[m, 0]))^2)=p*d)=>p∣(((Subscript[m, 0]))^2)))

(270)((((((((((Subscript[n, 0]))^2)))^2)))^2)⊥(Subscript[m, 0]))=>p∤(((((((((Subscript[n, 0]))^2)))^2)))^2)

(271)(((Subscript[n, 0]))^2)≠p*(((((((((Subscript[n, 0]))^2)))^2)))^2)

(272)((((((((((Subscript[n, 0]))^2)))^2)))^2)⊥(((Subscript[m, 0]))^2))=>p∤(((((((((Subscript[n, 0]))^2)))^2)))^2)

(273)((((((Subscript[n, 0]))^2)))^2)≠p*(((((((((Subscript[n, 0]))^2)))^2)))^2)

(274)(((((((Subscript[m, 0]))^2)))^2)=p*(((((((((Subscript[n, 0]))^2)))^2)))^2))=>p∣((((((Subscript[m, 0]))^2)))^2)

(275)((((((((((Subscript[n, 0]))^2)))^2)))^2)⊥((((((Subscript[m, 0]))^2)))^2))=>¬(p∣((((((Subscript[m, 0]))^2)))^2)∧p∣(((((((((Subscript[n, 0]))^2)))^2)))^2))

(276)((Subscript[d, 0])=p*(((((((((Subscript[n, 0]))^2)))^2)))^2))=>p∣(Subscript[d, 0])

(277)((((((((((Subscript[n, 0]))^2)))^2)))^2)⊥(Subscript[d, 0]))=>¬(p∣(Subscript[d, 0])∧p∣(((((((((Subscript[n, 0]))^2)))^2)))^2))

(278)((Subscript[d, 1])=p*(((((((((Subscript[n, 0]))^2)))^2)))^2))=>p∣(Subscript[d, 1])

(279)((((((((((Subscript[n, 0]))^2)))^2)))^2)⊥(Subscript[d, 1]))=>¬(p∣(Subscript[d, 1])∧p∣(((((((((Subscript[n, 0]))^2)))^2)))^2))

(28)p∣(((Subscript[m, 0]))^2)=>(Underscript[∃, d ])(nat[d]∧((((Subscript[m, 0]))^2)=p*d))

(280)(Underscript[∀, m ])(¬(((m^2)=p*(((Subscript[n, 0]))^2))∧(m=p*(((Subscript[n, 0]))^2))))

(281)((Sqrt[p]))≠(((Subscript[n, 0]))/(((Subscript[n, 0]))^2))

(282)(Subscript[m, 0])≠p*(((Subscript[n, 0]))^2)

(283)nat[((((((((((((Subscript[m, 0]))^2)))^2)))^2)))^2)]

(284)p∣(((((((((Subscript[m, 0]))^2)))^2)))^2)=>(Underscript[∃, d ])(nat[d]∧((((((((((Subscript[m, 0]))^2)))^2)))^2)=p*d))

(285)(Underscript[∀, d ])(nat[d]=>(((((((((((Subscript[m, 0]))^2)))^2)))^2)=p*d)=>p∣(((((((((Subscript[m, 0]))^2)))^2)))^2)))

(286)p∣((((((((((((Subscript[m, 0]))^2)))^2)))^2)))^2)=>p∣(((((((((Subscript[m, 0]))^2)))^2)))^2)

(287)(Underscript[∀, m ])(nat[m]=>((m⊥(((((((((Subscript[m, 0]))^2)))^2)))^2))=>¬(p∣(((((((((Subscript[m, 0]))^2)))^2)))^2)∧p∣m)))

(288)(Subscript[n, 0])≠p*(((((((((Subscript[m, 0]))^2)))^2)))^2)

(289)((((((((((Subscript[m, 0]))^2)))^2)))^2)⊥(Subscript[m, 0]))=>p∤(((((((((Subscript[m, 0]))^2)))^2)))^2)

(29)nat[((((((Subscript[m, 0]))^2)))^2)]

(290)(((Subscript[n, 0]))^2)≠p*(((((((((Subscript[m, 0]))^2)))^2)))^2)

(291)((((((((((Subscript[m, 0]))^2)))^2)))^2)⊥(((Subscript[m, 0]))^2))=>p∤(((((((((Subscript[m, 0]))^2)))^2)))^2)

(292)((((((Subscript[n, 0]))^2)))^2)≠p*(((((((((Subscript[m, 0]))^2)))^2)))^2)

(293)(((((((Subscript[m, 0]))^2)))^2)=p*(((((((((Subscript[m, 0]))^2)))^2)))^2))=>p∣((((((Subscript[m, 0]))^2)))^2)

(294)((((((((((Subscript[m, 0]))^2)))^2)))^2)⊥((((((Subscript[m, 0]))^2)))^2))=>¬(p∣((((((Subscript[m, 0]))^2)))^2)∧p∣(((((((((Subscript[m, 0]))^2)))^2)))^2))

(295)((Subscript[d, 0])=p*(((((((((Subscript[m, 0]))^2)))^2)))^2))=>p∣(Subscript[d, 0])

(296)((((((((((Subscript[m, 0]))^2)))^2)))^2)⊥(Subscript[d, 0]))=>¬(p∣(Subscript[d, 0])∧p∣(((((((((Subscript[m, 0]))^2)))^2)))^2))

(297)((Subscript[d, 1])=p*(((((((((Subscript[m, 0]))^2)))^2)))^2))=>p∣(Subscript[d, 1])

(298)((((((((((Subscript[m, 0]))^2)))^2)))^2)⊥(Subscript[d, 1]))=>¬(p∣(Subscript[d, 1])∧p∣(((((((((Subscript[m, 0]))^2)))^2)))^2))

(299)(Underscript[∀, m ])(¬(((m^2)=p*(((Subscript[n, 0]))^2))∧(m=p*(((Subscript[m, 0]))^2))))

(3)(nat[(Subscript[n, 0])]∧nat[(Subscript[m, 0])])∧((((Sqrt[p]))=(((Subscript[m, 0]))/((Subscript[n, 0]))))∧((Subscript[m, 0])⊥(Subscript[n, 0])))

(30)((((Subscript[n, 0]))^2)⊥(Subscript[m, 0]))=>¬(p∣(Subscript[m, 0])∧p∣(((Subscript[n, 0]))^2))

(300)((Sqrt[p]))≠(((Subscript[n, 0]))/(((Subscript[m, 0]))^2))

(301)(Subscript[m, 0])≠p*(((Subscript[m, 0]))^2)

(302)nat[((((((Subscript[d, 0]))^2)))^2)]

(303)p∣(((Subscript[d, 0]))^2)=>(Underscript[∃, d ])(nat[d]∧((((Subscript[d, 0]))^2)=p*d))

(304)(Underscript[∀, d ])(nat[d]=>(((((Subscript[d, 0]))^2)=p*d)=>p∣(((Subscript[d, 0]))^2)))

(305)p∣((((((Subscript[d, 0]))^2)))^2)=>p∣(((Subscript[d, 0]))^2)

(306)(Underscript[∀, m ])(nat[m]=>((m⊥(((Subscript[d, 0]))^2))=>¬(p∣(((Subscript[d, 0]))^2)∧p∣m)))

(307)(Subscript[n, 0])≠p*(((Subscript[d, 0]))^2)

(308)((((Subscript[d, 0]))^2)⊥(Subscript[m, 0]))=>p∤(((Subscript[d, 0]))^2)

(309)(((Subscript[n, 0]))^2)≠p*(((Subscript[d, 0]))^2)

(3.1)nat[(Subscript[n, 0])]∧nat[(Subscript[m, 0])]

(31)((Subscript[m, 0])=p*(((Subscript[n, 0]))^2))=>p∣(Subscript[m, 0])

(310)((((Subscript[d, 0]))^2)⊥(((Subscript[m, 0]))^2))=>p∤(((Subscript[d, 0]))^2)

(3.1.1)nat[(Subscript[n, 0])]

(311)((((((Subscript[n, 0]))^2)))^2)≠p*(((Subscript[d, 0]))^2)

(3.1.2)nat[(Subscript[m, 0])]

(312)(((((((Subscript[m, 0]))^2)))^2)=p*(((Subscript[d, 0]))^2))=>p∣((((((Subscript[m, 0]))^2)))^2)

(313)((((Subscript[d, 0]))^2)⊥((((((Subscript[m, 0]))^2)))^2))=>¬(p∣((((((Subscript[m, 0]))^2)))^2)∧p∣(((Subscript[d, 0]))^2))

(314)((Subscript[d, 0])=p*(((Subscript[d, 0]))^2))=>p∣(Subscript[d, 0])

(315)((((Subscript[d, 0]))^2)⊥(Subscript[d, 0]))=>¬(p∣(Subscript[d, 0])∧p∣(((Subscript[d, 0]))^2))

(316)((Subscript[d, 1])=p*(((Subscript[d, 0]))^2))=>p∣(Subscript[d, 1])

(317)((((Subscript[d, 0]))^2)⊥(Subscript[d, 1]))=>¬(p∣(Subscript[d, 1])∧p∣(((Subscript[d, 0]))^2))

(318)(Underscript[∀, k ])(((Subscript[n, 0])=p*k)=>((((Subscript[d, 0]))^2)=p*(k^2)))

(319)nat[(((Subscript[n, 0]))^2)]∧nat[(((Subscript[d, 0]))^2)]=>p∣(((Subscript[n, 0]))^2)

(3.2)(((Sqrt[p]))=(((Subscript[m, 0]))/((Subscript[n, 0]))))∧((Subscript[m, 0])⊥(Subscript[n, 0]))

(32)((((Subscript[n, 0]))^2)⊥(Subscript[n, 0]))=>¬(p∣(Subscript[n, 0])∧p∣(((Subscript[n, 0]))^2))

(320)¬nat[(((Subscript[d, 0]))^2)]

(3.2.1)((Sqrt[p]))=(((Subscript[m, 0]))/((Subscript[n, 0])))

(321)nat[((((((Subscript[d, 1]))^2)))^2)]

(3.2.2)(Subscript[m, 0])⊥(Subscript[n, 0])

(322)p∣(((Subscript[d, 1]))^2)=>(Underscript[∃, d ])(nat[d]∧((((Subscript[d, 1]))^2)=p*d))

(323)(Underscript[∀, d ])(nat[d]=>(((((Subscript[d, 1]))^2)=p*d)=>p∣(((Subscript[d, 1]))^2)))

(324)p∣((((((Subscript[d, 1]))^2)))^2)=>p∣(((Subscript[d, 1]))^2)

(325)(Underscript[∀, m ])(nat[m]=>((m⊥(((Subscript[d, 1]))^2))=>¬(p∣(((Subscript[d, 1]))^2)∧p∣m)))

(326)(Subscript[n, 0])≠p*(((Subscript[d, 1]))^2)

(327)((((Subscript[d, 1]))^2)⊥(Subscript[m, 0]))=>p∤(((Subscript[d, 1]))^2)

(328)(((Subscript[n, 0]))^2)≠p*(((Subscript[d, 1]))^2)

(329)((((Subscript[d, 1]))^2)⊥(((Subscript[m, 0]))^2))=>p∤(((Subscript[d, 1]))^2)

(33)((Subscript[n, 0])=p*(((Subscript[n, 0]))^2))=>p∣(Subscript[n, 0])

(330)((((((Subscript[n, 0]))^2)))^2)≠p*(((Subscript[d, 1]))^2)

(331)(((((((Subscript[m, 0]))^2)))^2)=p*(((Subscript[d, 1]))^2))=>p∣((((((Subscript[m, 0]))^2)))^2)

(332)((((Subscript[d, 1]))^2)⊥((((((Subscript[m, 0]))^2)))^2))=>¬(p∣((((((Subscript[m, 0]))^2)))^2)∧p∣(((Subscript[d, 1]))^2))

(333)((Subscript[d, 0])=p*(((Subscript[d, 1]))^2))=>p∣(Subscript[d, 0])

(334)((((Subscript[d, 1]))^2)⊥(Subscript[d, 0]))=>¬(p∣(Subscript[d, 0])∧p∣(((Subscript[d, 1]))^2))

(335)((Subscript[d, 1])=p*(((Subscript[d, 1]))^2))=>p∣(Subscript[d, 1])

(336)((((Subscript[d, 1]))^2)⊥(Subscript[d, 1]))=>¬(p∣(Subscript[d, 1])∧p∣(((Subscript[d, 1]))^2))

(34)(Underscript[∀, m ])(nat[m]=>((m⊥(((Subscript[n, 0]))^2))=>¬(p∣(((Subscript[n, 0]))^2)∧p∣m)))

(35)p∣((((((Subscript[n, 0]))^2)))^2)=>p∣(((Subscript[n, 0]))^2)

(36)(Underscript[∀, d ])(nat[d]=>(((((Subscript[n, 0]))^2)=p*d)=>p∣(((Subscript[n, 0]))^2)))

(37)p∣(((Subscript[n, 0]))^2)=>(Underscript[∃, d ])(nat[d]∧((((Subscript[n, 0]))^2)=p*d))

(38)nat[((((((Subscript[n, 0]))^2)))^2)]

(39)nat[(Subscript[m, 0])]=>¬(p∣(Subscript[n, 0])∧p∣(Subscript[m, 0]))

(4)nat[(Subscript[n, 0])]∧nat[(Subscript[m, 0])]=>¬(p∣(Subscript[n, 0])∧p∣(Subscript[m, 0]))

(40)((Subscript[m, 0])⊥(Subscript[m, 0]))=>¬(p∣(Subscript[m, 0])∧p∣(Subscript[m, 0]))

(41)((Subscript[m, 0])=p*(Subscript[m, 0]))=>p∣(Subscript[m, 0])

(42)((Subscript[m, 0])⊥(Subscript[n, 0]))=>¬(p∣(Subscript[n, 0])∧p∣(Subscript[m, 0]))

(43)((Subscript[n, 0])=p*(Subscript[m, 0]))=>p∣(Subscript[n, 0])

(44)((Subscript[n, 0])⊥(Subscript[m, 0]))=>¬(p∣(Subscript[m, 0])∧p∣(Subscript[n, 0]))

(45)((Subscript[m, 0])=p*(Subscript[n, 0]))=>p∣(Subscript[m, 0])

(46)((Subscript[n, 0])⊥(Subscript[n, 0]))=>¬(p∣(Subscript[n, 0])∧p∣(Subscript[n, 0]))

(47)((Subscript[n, 0])=p*(Subscript[n, 0]))=>p∣(Subscript[n, 0])

(48)¬(p∣(Subscript[n, 0])∧p∣(Subscript[m, 0]))

(49)p∤(Subscript[n, 0])∨p∤(Subscript[m, 0])

(5)(((Subscript[m, 0]))^2)=p*(((Subscript[n, 0]))^2)

(50)nat[(((Subscript[m, 0]))^2)]=>p∣(((Subscript[m, 0]))^2)

(51)p∣(((Subscript[m, 0]))^2)

(52)p∣(Subscript[m, 0])

(53)(Underscript[∃, d ])(nat[d]∧((Subscript[m, 0])=p*d))

(54)(Underscript[∀, m ])(nat[m]=>((m⊥(Subscript[m, 0]))=>p∤m))

(55)p∤(Subscript[n, 0])

(56)(Underscript[∀, d ])(nat[d]=>(Subscript[n, 0])≠p*d)

(57)p∤(((Subscript[n, 0]))^2)

(58)(Underscript[∀, d ])(nat[d]=>(((Subscript[n, 0]))^2)≠p*d)

(59)p∤((((((Subscript[n, 0]))^2)))^2)

(6)(Underscript[∀, m ])(nat[m]=>((m⊥(Subscript[m, 0]))=>¬(p∣(Subscript[m, 0])∧p∣m)))

(60)(Subscript[n, 0])≠p*(Subscript[n, 0])

(61)(Subscript[n, 0])≠p*(Subscript[m, 0])

(62)(Subscript[n, 0])≠p*(((Subscript[n, 0]))^2)

(63)(Subscript[n, 0])≠p*(((Subscript[m, 0]))^2)

(64)¬((Subscript[m, 0])⊥(Subscript[m, 0]))

(65)((((Subscript[m, 0]))^2)⊥(Subscript[m, 0]))=>p∤(((Subscript[m, 0]))^2)

(66)(Underscript[∃, d ])(nat[d]∧((((Subscript[m, 0]))^2)=p*d))

(67)(Underscript[∀, m ])(nat[m]=>((m⊥(((Subscript[m, 0]))^2))=>p∤m))

(68)¬((((Subscript[m, 0]))^2)⊥(Subscript[m, 0]))

(69)nat[(Subscript[d, 0])]∧((Subscript[m, 0])=p*(Subscript[d, 0]))

(69.1)nat[(Subscript[d, 0])]

(69.2)(Subscript[m, 0])=p*(Subscript[d, 0])

(7)p∣(((Subscript[m, 0]))^2)=>p∣(Subscript[m, 0])

(70)nat[(Subscript[d, 1])]∧((((Subscript[m, 0]))^2)=p*(Subscript[d, 1]))

(70.1)nat[(Subscript[d, 1])]

(70.2)(((Subscript[m, 0]))^2)=p*(Subscript[d, 1])

(71)nat[(((Subscript[m, 0]))^2)]∧nat[(Subscript[d, 1])]=>p∣(((Subscript[m, 0]))^2)

(72)(Underscript[∀, n ])((((((((Subscript[m, 0]))^2)))^2)=p*(n^2))=>((n^2)=p*(((Subscript[d, 1]))^2)))

(73)((Subscript[d, 1])⊥(((Subscript[m, 0]))^2))=>p∤(Subscript[d, 1])

(74)(((Subscript[n, 0]))^2)≠p*(Subscript[d, 1])

(75)((Subscript[d, 1])⊥(Subscript[m, 0]))=>p∤(Subscript[d, 1])

(76)(Subscript[n, 0])≠p*(Subscript[d, 1])

(77)(Underscript[∀, m ])(nat[m]=>((m⊥(Subscript[d, 1]))=>¬(p∣(Subscript[d, 1])∧p∣m)))

(78)p∣(((Subscript[d, 1]))^2)=>p∣(Subscript[d, 1])

(79)(Underscript[∀, d ])(nat[d]=>(((Subscript[d, 1])=p*d)=>p∣(Subscript[d, 1])))

(8)(Underscript[∀, d ])(nat[d]=>(((Subscript[m, 0])=p*d)=>p∣(Subscript[m, 0])))

(80)p∣(Subscript[d, 1])=>(Underscript[∃, d ])(nat[d]∧((Subscript[d, 1])=p*d))

(81)nat[(((Subscript[d, 1]))^2)]

(82)(((Subscript[n, 0]))^2)=p*(((Subscript[d, 0]))^2)

(83)nat[(Subscript[m, 0])]∧nat[(Subscript[d, 0])]=>p∣(Subscript[m, 0])

(84)(Underscript[∀, n ])(((((Subscript[m, 0]))^2)=p*(n^2))=>((n^2)=p*(((Subscript[d, 0]))^2)))

(85)((Subscript[d, 0])⊥(((Subscript[m, 0]))^2))=>p∤(Subscript[d, 0])

(86)(((Subscript[n, 0]))^2)≠p*(Subscript[d, 0])

(87)((Subscript[d, 0])⊥(Subscript[m, 0]))=>p∤(Subscript[d, 0])

(88)(Subscript[n, 0])≠p*(Subscript[d, 0])

(89)(Underscript[∀, m ])(nat[m]=>((m⊥(Subscript[d, 0]))=>¬(p∣(Subscript[d, 0])∧p∣m)))

(9)p∣(Subscript[m, 0])=>(Underscript[∃, d ])(nat[d]∧((Subscript[m, 0])=p*d))

(90)p∣(((Subscript[d, 0]))^2)=>p∣(Subscript[d, 0])

(91)(Underscript[∀, d ])(nat[d]=>(((Subscript[d, 0])=p*d)=>p∣(Subscript[d, 0])))

(92)p∣(Subscript[d, 0])=>(Underscript[∃, d ])(nat[d]∧((Subscript[d, 0])=p*d))

(93)nat[(((Subscript[d, 0]))^2)]

(94)(((((((Subscript[m, 0]))^2)))^2)⊥(((Subscript[m, 0]))^2))=>p∤((((((Subscript[m, 0]))^2)))^2)

(95)(((Subscript[n, 0]))^2)≠p*((((((Subscript[m, 0]))^2)))^2)

(96)(((((((Subscript[m, 0]))^2)))^2)⊥(Subscript[m, 0]))=>p∤((((((Subscript[m, 0]))^2)))^2)

(97)(Subscript[n, 0])≠p*((((((Subscript[m, 0]))^2)))^2)

(98)(Underscript[∀, m ])(nat[m]=>((m⊥((((((Subscript[m, 0]))^2)))^2))=>¬(p∣((((((Subscript[m, 0]))^2)))^2)∧p∣m)))

(99)p∣(((((((((Subscript[m, 0]))^2)))^2)))^2)=>p∣((((((Subscript[m, 0]))^2)))^2)

(a contradiction)False

(Definition (Divisible): 1)(Underscript[∀, d,n])(nat[n]∧nat[d]=>((n=p*d)=>p∣n))

(Definition (Divisible): 2)(Underscript[∀, n ])(nat[n]=>(p∣n=>(Underscript[∃, d ])(nat[d]∧(n=p*d))))

(Definition (Rational))(Underscript[∀, q ])(rat[q]⇔(Underscript[∃, m,n])((nat[n]∧nat[m])∧((q=(m/n))∧(m⊥n))))

(Lemma (Coprime for Two))(Underscript[∀, m,n])(nat[n]∧nat[m]=>((m⊥n)=>¬(p∣n∧p∣m)))

(Lemma (Euclid))(Underscript[∀, m ])(nat[m]=>(p∣(m^2)=>p∣m))

(Lemma (Multiply Root Equation))(Underscript[∀, m,n])((((Sqrt[p]))=(m/n))=>((m^2)=p*(n^2)))

(Lemma (Simplify by Cancelling))(Underscript[∀, k,m,n])(((m^2)=p*(n^2))∧(m=p*k)=>((n^2)=p*(k^2)))

(Lemma (Squares Preserve Naturals))(Underscript[∀, n ])(nat[n]=>nat[(n^2)])

(Theorem (Root Irrational))¬ rat[(Sqrt[p])]