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)p∣(((Subscript[m, 0]))^2)=>p∣(Subscript[m, 0])

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(134)nat[(Subscript[m, 0])]=>(((Subscript[m, 0])⊥(Subscript[m, 0]))=>p∤(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)((Subscript[d, 1])⊥(((Subscript[n, 0]))^2))=>¬(p∣(((Subscript[n, 0]))^2)∧p∣(Subscript[d, 1]))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(299)nat[(((Subscript[m, 0]))^2)]=>(((((Subscript[d, 0]))^2)⊥(((Subscript[m, 0]))^2))=>p∤(((Subscript[d, 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[m, 0])=p*(((Subscript[n, 0]))^2))=>p∣(Subscript[m, 0])

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

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

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

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

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

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

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

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

(308)((((Subscript[d, 0]))^2)⊥(((Subscript[m, 0]))^2))=>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)(Underscript[∀, m ])(nat[m]=>((m⊥(((Subscript[n, 0]))^2))=>¬(p∣(((Subscript[n, 0]))^2)∧p∣m)))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(324)¬(nat[(((Subscript[n, 0]))^2)]∧nat[(((Subscript[d, 0]))^2)])

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(353)nat[(Subscript[n, 0])]=>(Subscript[n, 0])≠p*(Subscript[d, 2])

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(373)nat[(Subscript[d, 2])]=>p∣(Subscript[m, 0])

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(403)nat[((((((Subscript[n, 0]))^2)))^2)]=>((((((Subscript[n, 0]))^2)))^2)≠p*(((Subscript[d, 1]))^2)

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

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

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

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

(408)nat[(Subscript[n, 0])]=>(Subscript[n, 0])≠p*(((Subscript[d, 1]))^2)

(409)nat[(((Subscript[n, 0]))^2)]=>(((Subscript[n, 0]))^2)≠p*(((Subscript[d, 1]))^2)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(440)nat[((((((Subscript[n, 0]))^2)))^2)]=>((((((Subscript[n, 0]))^2)))^2)≠p*(Subscript[d, 3])

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

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

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

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

(445)nat[(Subscript[n, 0])]=>(Subscript[n, 0])≠p*(Subscript[d, 3])

(446)nat[(((Subscript[n, 0]))^2)]=>(((Subscript[n, 0]))^2)≠p*(Subscript[d, 3])

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(469)nat[((((((Subscript[n, 0]))^2)))^2)]=>((((((Subscript[n, 0]))^2)))^2)≠p*(((((((((Subscript[n, 0]))^2)))^2)))^2)

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

(470)nat[((((((Subscript[n, 0]))^2)))^2)]=>((((((Subscript[n, 0]))^2)))^2)≠p*(((((((((Subscript[m, 0]))^2)))^2)))^2)

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

(472)nat[((((((Subscript[n, 0]))^2)))^2)]=>((((((Subscript[n, 0]))^2)))^2)≠p*(Subscript[d, 1])

(473)nat[((((((Subscript[n, 0]))^2)))^2)]=>((((((Subscript[n, 0]))^2)))^2)≠p*((((((Subscript[n, 0]))^2)))^2)

(474)nat[((((((Subscript[n, 0]))^2)))^2)]=>((((((Subscript[n, 0]))^2)))^2)≠p*((((((Subscript[m, 0]))^2)))^2)

(475)nat[((((((Subscript[n, 0]))^2)))^2)]=>((((((Subscript[n, 0]))^2)))^2)≠p*(((Subscript[n, 0]))^2)

(476)nat[((((((Subscript[n, 0]))^2)))^2)]=>((((((Subscript[n, 0]))^2)))^2)≠p*(((Subscript[m, 0]))^2)

(477)nat[((((((Subscript[n, 0]))^2)))^2)]=>((((((Subscript[n, 0]))^2)))^2)≠p*(Subscript[n, 0])

(478)nat[((((((Subscript[n, 0]))^2)))^2)]=>((((((Subscript[n, 0]))^2)))^2)≠p*(Subscript[m, 0])

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(503)nat[(Subscript[n, 0])]=>(Subscript[n, 0])≠p*(((((((((Subscript[n, 0]))^2)))^2)))^2)

(504)nat[(((Subscript[n, 0]))^2)]=>(((Subscript[n, 0]))^2)≠p*(((((((((Subscript[n, 0]))^2)))^2)))^2)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(542)nat[(Subscript[n, 0])]=>(Subscript[n, 0])≠p*(((((((((Subscript[m, 0]))^2)))^2)))^2)

(543)nat[(((Subscript[n, 0]))^2)]=>(((Subscript[n, 0]))^2)≠p*(((((((((Subscript[m, 0]))^2)))^2)))^2)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(561)nat[(Subscript[n, 0])]=>(Subscript[n, 0])≠p*(Subscript[d, 0])

(562)nat[(Subscript[n, 0])]=>(Subscript[n, 0])≠p*(Subscript[d, 1])

(563)nat[(Subscript[n, 0])]=>(Subscript[n, 0])≠p*((((((Subscript[n, 0]))^2)))^2)

(564)nat[(Subscript[n, 0])]=>(Subscript[n, 0])≠p*((((((Subscript[m, 0]))^2)))^2)

(565)nat[(Subscript[n, 0])]=>(Subscript[n, 0])≠p*(((Subscript[n, 0]))^2)

(566)nat[(Subscript[n, 0])]=>(Subscript[n, 0])≠p*(((Subscript[m, 0]))^2)

(567)nat[(Subscript[n, 0])]=>(Subscript[n, 0])≠p*(Subscript[n, 0])

(568)nat[(Subscript[n, 0])]=>(Subscript[n, 0])≠p*(Subscript[m, 0])

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

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

(570)nat[(((Subscript[n, 0]))^2)]=>(((Subscript[n, 0]))^2)≠p*(Subscript[d, 1])

(571)nat[(((Subscript[n, 0]))^2)]=>(((Subscript[n, 0]))^2)≠p*((((((Subscript[n, 0]))^2)))^2)

(572)nat[(((Subscript[n, 0]))^2)]=>(((Subscript[n, 0]))^2)≠p*((((((Subscript[m, 0]))^2)))^2)

(573)nat[(((Subscript[n, 0]))^2)]=>(((Subscript[n, 0]))^2)≠p*(((Subscript[n, 0]))^2)

(574)nat[(((Subscript[n, 0]))^2)]=>(((Subscript[n, 0]))^2)≠p*(((Subscript[m, 0]))^2)

(575)nat[(((Subscript[n, 0]))^2)]=>(((Subscript[n, 0]))^2)≠p*(Subscript[n, 0])

(576)nat[(((Subscript[n, 0]))^2)]=>(((Subscript[n, 0]))^2)≠p*(Subscript[m, 0])

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(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])]