# Metamath Proof Explorer

## Theorem difsqpwdvds

Description: If the difference of two squares is a power of a prime, the prime divides twice the second squared number. (Contributed by AV, 13-Aug-2021)

Ref Expression
Assertion difsqpwdvds ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\to \left({{C}}^{{D}}={{A}}^{2}-{{B}}^{2}\to {C}\parallel 2{B}\right)$

### Proof

Step Hyp Ref Expression
1 nn0cn ${⊢}{A}\in {ℕ}_{0}\to {A}\in ℂ$
2 nn0cn ${⊢}{B}\in {ℕ}_{0}\to {B}\in ℂ$
3 1 2 anim12i ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\right)\to \left({A}\in ℂ\wedge {B}\in ℂ\right)$
4 3 3adant3 ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\to \left({A}\in ℂ\wedge {B}\in ℂ\right)$
5 subsq ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {{A}}^{2}-{{B}}^{2}=\left({A}+{B}\right)\left({A}-{B}\right)$
6 4 5 syl ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\to {{A}}^{2}-{{B}}^{2}=\left({A}+{B}\right)\left({A}-{B}\right)$
7 6 adantr ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\to {{A}}^{2}-{{B}}^{2}=\left({A}+{B}\right)\left({A}-{B}\right)$
8 7 eqeq2d ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\to \left({{C}}^{{D}}={{A}}^{2}-{{B}}^{2}↔{{C}}^{{D}}=\left({A}+{B}\right)\left({A}-{B}\right)\right)$
9 simprl ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\to {C}\in ℙ$
10 nn0z ${⊢}{A}\in {ℕ}_{0}\to {A}\in ℤ$
11 nn0z ${⊢}{B}\in {ℕ}_{0}\to {B}\in ℤ$
12 10 11 anim12i ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\right)\to \left({A}\in ℤ\wedge {B}\in ℤ\right)$
13 zaddcl ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {A}+{B}\in ℤ$
14 12 13 syl ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\right)\to {A}+{B}\in ℤ$
15 14 3adant3 ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\to {A}+{B}\in ℤ$
16 nn0re ${⊢}{B}\in {ℕ}_{0}\to {B}\in ℝ$
17 16 adantl ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\right)\to {B}\in ℝ$
18 1red ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\right)\to 1\in ℝ$
19 nn0re ${⊢}{A}\in {ℕ}_{0}\to {A}\in ℝ$
20 19 adantr ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\right)\to {A}\in ℝ$
21 17 18 20 ltaddsub2d ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\right)\to \left({B}+1<{A}↔1<{A}-{B}\right)$
22 simpr ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\right)\to {B}\in {ℕ}_{0}$
23 20 22 18 3jca ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\right)\to \left({A}\in ℝ\wedge {B}\in {ℕ}_{0}\wedge 1\in ℝ\right)$
24 difgtsumgt ${⊢}\left({A}\in ℝ\wedge {B}\in {ℕ}_{0}\wedge 1\in ℝ\right)\to \left(1<{A}-{B}\to 1<{A}+{B}\right)$
25 23 24 syl ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\right)\to \left(1<{A}-{B}\to 1<{A}+{B}\right)$
26 21 25 sylbid ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\right)\to \left({B}+1<{A}\to 1<{A}+{B}\right)$
27 26 3impia ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\to 1<{A}+{B}$
28 eluz2b1 ${⊢}{A}+{B}\in {ℤ}_{\ge 2}↔\left({A}+{B}\in ℤ\wedge 1<{A}+{B}\right)$
29 15 27 28 sylanbrc ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\to {A}+{B}\in {ℤ}_{\ge 2}$
30 29 adantr ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\to {A}+{B}\in {ℤ}_{\ge 2}$
31 simprr ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\to {D}\in {ℕ}_{0}$
32 9 30 31 3jca ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\to \left({C}\in ℙ\wedge {A}+{B}\in {ℤ}_{\ge 2}\wedge {D}\in {ℕ}_{0}\right)$
33 32 adantr ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\wedge {{C}}^{{D}}=\left({A}+{B}\right)\left({A}-{B}\right)\right)\to \left({C}\in ℙ\wedge {A}+{B}\in {ℤ}_{\ge 2}\wedge {D}\in {ℕ}_{0}\right)$
34 zsubcl ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {A}-{B}\in ℤ$
35 13 34 jca ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left({A}+{B}\in ℤ\wedge {A}-{B}\in ℤ\right)$
36 12 35 syl ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\right)\to \left({A}+{B}\in ℤ\wedge {A}-{B}\in ℤ\right)$
37 36 3adant3 ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\to \left({A}+{B}\in ℤ\wedge {A}-{B}\in ℤ\right)$
38 dvdsmul1 ${⊢}\left({A}+{B}\in ℤ\wedge {A}-{B}\in ℤ\right)\to \left({A}+{B}\right)\parallel \left({A}+{B}\right)\left({A}-{B}\right)$
39 37 38 syl ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\to \left({A}+{B}\right)\parallel \left({A}+{B}\right)\left({A}-{B}\right)$
40 39 ad2antrr ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\wedge {{C}}^{{D}}=\left({A}+{B}\right)\left({A}-{B}\right)\right)\to \left({A}+{B}\right)\parallel \left({A}+{B}\right)\left({A}-{B}\right)$
41 breq2 ${⊢}{{C}}^{{D}}=\left({A}+{B}\right)\left({A}-{B}\right)\to \left(\left({A}+{B}\right)\parallel {{C}}^{{D}}↔\left({A}+{B}\right)\parallel \left({A}+{B}\right)\left({A}-{B}\right)\right)$
42 41 adantl ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\wedge {{C}}^{{D}}=\left({A}+{B}\right)\left({A}-{B}\right)\right)\to \left(\left({A}+{B}\right)\parallel {{C}}^{{D}}↔\left({A}+{B}\right)\parallel \left({A}+{B}\right)\left({A}-{B}\right)\right)$
43 40 42 mpbird ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\wedge {{C}}^{{D}}=\left({A}+{B}\right)\left({A}-{B}\right)\right)\to \left({A}+{B}\right)\parallel {{C}}^{{D}}$
44 dvdsprmpweqnn ${⊢}\left({C}\in ℙ\wedge {A}+{B}\in {ℤ}_{\ge 2}\wedge {D}\in {ℕ}_{0}\right)\to \left(\left({A}+{B}\right)\parallel {{C}}^{{D}}\to \exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}{A}+{B}={{C}}^{{m}}\right)$
45 33 43 44 sylc ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\wedge {{C}}^{{D}}=\left({A}+{B}\right)\left({A}-{B}\right)\right)\to \exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}{A}+{B}={{C}}^{{m}}$
46 prmz ${⊢}{C}\in ℙ\to {C}\in ℤ$
47 iddvdsexp ${⊢}\left({C}\in ℤ\wedge {m}\in ℕ\right)\to {C}\parallel {{C}}^{{m}}$
48 46 47 sylan ${⊢}\left({C}\in ℙ\wedge {m}\in ℕ\right)\to {C}\parallel {{C}}^{{m}}$
49 breq2 ${⊢}{A}+{B}={{C}}^{{m}}\to \left({C}\parallel \left({A}+{B}\right)↔{C}\parallel {{C}}^{{m}}\right)$
50 48 49 syl5ibrcom ${⊢}\left({C}\in ℙ\wedge {m}\in ℕ\right)\to \left({A}+{B}={{C}}^{{m}}\to {C}\parallel \left({A}+{B}\right)\right)$
51 50 rexlimdva ${⊢}{C}\in ℙ\to \left(\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}{A}+{B}={{C}}^{{m}}\to {C}\parallel \left({A}+{B}\right)\right)$
52 51 adantr ${⊢}\left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\to \left(\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}{A}+{B}={{C}}^{{m}}\to {C}\parallel \left({A}+{B}\right)\right)$
53 52 adantl ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\to \left(\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}{A}+{B}={{C}}^{{m}}\to {C}\parallel \left({A}+{B}\right)\right)$
54 53 adantr ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\wedge {{C}}^{{D}}=\left({A}+{B}\right)\left({A}-{B}\right)\right)\to \left(\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}{A}+{B}={{C}}^{{m}}\to {C}\parallel \left({A}+{B}\right)\right)$
55 12 34 syl ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\right)\to {A}-{B}\in ℤ$
56 55 3adant3 ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\to {A}-{B}\in ℤ$
57 21 biimp3a ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\to 1<{A}-{B}$
58 eluz2b1 ${⊢}{A}-{B}\in {ℤ}_{\ge 2}↔\left({A}-{B}\in ℤ\wedge 1<{A}-{B}\right)$
59 56 57 58 sylanbrc ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\to {A}-{B}\in {ℤ}_{\ge 2}$
60 59 adantr ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\to {A}-{B}\in {ℤ}_{\ge 2}$
61 9 60 31 3jca ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\to \left({C}\in ℙ\wedge {A}-{B}\in {ℤ}_{\ge 2}\wedge {D}\in {ℕ}_{0}\right)$
62 61 adantr ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\wedge {{C}}^{{D}}=\left({A}+{B}\right)\left({A}-{B}\right)\right)\to \left({C}\in ℙ\wedge {A}-{B}\in {ℤ}_{\ge 2}\wedge {D}\in {ℕ}_{0}\right)$
63 dvdsmul2 ${⊢}\left({A}+{B}\in ℤ\wedge {A}-{B}\in ℤ\right)\to \left({A}-{B}\right)\parallel \left({A}+{B}\right)\left({A}-{B}\right)$
64 37 63 syl ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\to \left({A}-{B}\right)\parallel \left({A}+{B}\right)\left({A}-{B}\right)$
65 64 ad2antrr ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\wedge {{C}}^{{D}}=\left({A}+{B}\right)\left({A}-{B}\right)\right)\to \left({A}-{B}\right)\parallel \left({A}+{B}\right)\left({A}-{B}\right)$
66 breq2 ${⊢}{{C}}^{{D}}=\left({A}+{B}\right)\left({A}-{B}\right)\to \left(\left({A}-{B}\right)\parallel {{C}}^{{D}}↔\left({A}-{B}\right)\parallel \left({A}+{B}\right)\left({A}-{B}\right)\right)$
67 66 adantl ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\wedge {{C}}^{{D}}=\left({A}+{B}\right)\left({A}-{B}\right)\right)\to \left(\left({A}-{B}\right)\parallel {{C}}^{{D}}↔\left({A}-{B}\right)\parallel \left({A}+{B}\right)\left({A}-{B}\right)\right)$
68 65 67 mpbird ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\wedge {{C}}^{{D}}=\left({A}+{B}\right)\left({A}-{B}\right)\right)\to \left({A}-{B}\right)\parallel {{C}}^{{D}}$
69 dvdsprmpweqnn ${⊢}\left({C}\in ℙ\wedge {A}-{B}\in {ℤ}_{\ge 2}\wedge {D}\in {ℕ}_{0}\right)\to \left(\left({A}-{B}\right)\parallel {{C}}^{{D}}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}-{B}={{C}}^{{n}}\right)$
70 62 68 69 sylc ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\wedge {{C}}^{{D}}=\left({A}+{B}\right)\left({A}-{B}\right)\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}-{B}={{C}}^{{n}}$
71 iddvdsexp ${⊢}\left({C}\in ℤ\wedge {n}\in ℕ\right)\to {C}\parallel {{C}}^{{n}}$
72 46 71 sylan ${⊢}\left({C}\in ℙ\wedge {n}\in ℕ\right)\to {C}\parallel {{C}}^{{n}}$
73 breq2 ${⊢}{A}-{B}={{C}}^{{n}}\to \left({C}\parallel \left({A}-{B}\right)↔{C}\parallel {{C}}^{{n}}\right)$
74 72 73 syl5ibrcom ${⊢}\left({C}\in ℙ\wedge {n}\in ℕ\right)\to \left({A}-{B}={{C}}^{{n}}\to {C}\parallel \left({A}-{B}\right)\right)$
75 74 rexlimdva ${⊢}{C}\in ℙ\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}-{B}={{C}}^{{n}}\to {C}\parallel \left({A}-{B}\right)\right)$
76 75 adantr ${⊢}\left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}-{B}={{C}}^{{n}}\to {C}\parallel \left({A}-{B}\right)\right)$
77 76 adantl ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}-{B}={{C}}^{{n}}\to {C}\parallel \left({A}-{B}\right)\right)$
78 77 adantr ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\wedge {{C}}^{{D}}=\left({A}+{B}\right)\left({A}-{B}\right)\right)\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}-{B}={{C}}^{{n}}\to {C}\parallel \left({A}-{B}\right)\right)$
79 46 adantr ${⊢}\left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\to {C}\in ℤ$
80 37 79 anim12ci ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\to \left({C}\in ℤ\wedge \left({A}+{B}\in ℤ\wedge {A}-{B}\in ℤ\right)\right)$
81 3anass ${⊢}\left({C}\in ℤ\wedge {A}+{B}\in ℤ\wedge {A}-{B}\in ℤ\right)↔\left({C}\in ℤ\wedge \left({A}+{B}\in ℤ\wedge {A}-{B}\in ℤ\right)\right)$
82 80 81 sylibr ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\to \left({C}\in ℤ\wedge {A}+{B}\in ℤ\wedge {A}-{B}\in ℤ\right)$
83 dvds2sub ${⊢}\left({C}\in ℤ\wedge {A}+{B}\in ℤ\wedge {A}-{B}\in ℤ\right)\to \left(\left({C}\parallel \left({A}+{B}\right)\wedge {C}\parallel \left({A}-{B}\right)\right)\to {C}\parallel \left({A}+{B}-\left({A}-{B}\right)\right)\right)$
84 82 83 syl ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\to \left(\left({C}\parallel \left({A}+{B}\right)\wedge {C}\parallel \left({A}-{B}\right)\right)\to {C}\parallel \left({A}+{B}-\left({A}-{B}\right)\right)\right)$
85 1 3ad2ant1 ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\to {A}\in ℂ$
86 2 3ad2ant2 ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\to {B}\in ℂ$
87 85 86 86 pnncand ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\to {A}+{B}-\left({A}-{B}\right)={B}+{B}$
88 2 2timesd ${⊢}{B}\in {ℕ}_{0}\to 2{B}={B}+{B}$
89 88 eqcomd ${⊢}{B}\in {ℕ}_{0}\to {B}+{B}=2{B}$
90 89 3ad2ant2 ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\to {B}+{B}=2{B}$
91 87 90 eqtrd ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\to {A}+{B}-\left({A}-{B}\right)=2{B}$
92 91 breq2d ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\to \left({C}\parallel \left({A}+{B}-\left({A}-{B}\right)\right)↔{C}\parallel 2{B}\right)$
93 92 biimpd ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\to \left({C}\parallel \left({A}+{B}-\left({A}-{B}\right)\right)\to {C}\parallel 2{B}\right)$
94 93 adantr ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\to \left({C}\parallel \left({A}+{B}-\left({A}-{B}\right)\right)\to {C}\parallel 2{B}\right)$
95 84 94 syld ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\to \left(\left({C}\parallel \left({A}+{B}\right)\wedge {C}\parallel \left({A}-{B}\right)\right)\to {C}\parallel 2{B}\right)$
96 95 expcomd ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\to \left({C}\parallel \left({A}-{B}\right)\to \left({C}\parallel \left({A}+{B}\right)\to {C}\parallel 2{B}\right)\right)$
97 96 adantr ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\wedge {{C}}^{{D}}=\left({A}+{B}\right)\left({A}-{B}\right)\right)\to \left({C}\parallel \left({A}-{B}\right)\to \left({C}\parallel \left({A}+{B}\right)\to {C}\parallel 2{B}\right)\right)$
98 78 97 syld ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\wedge {{C}}^{{D}}=\left({A}+{B}\right)\left({A}-{B}\right)\right)\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}-{B}={{C}}^{{n}}\to \left({C}\parallel \left({A}+{B}\right)\to {C}\parallel 2{B}\right)\right)$
99 70 98 mpd ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\wedge {{C}}^{{D}}=\left({A}+{B}\right)\left({A}-{B}\right)\right)\to \left({C}\parallel \left({A}+{B}\right)\to {C}\parallel 2{B}\right)$
100 54 99 syld ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\wedge {{C}}^{{D}}=\left({A}+{B}\right)\left({A}-{B}\right)\right)\to \left(\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}{A}+{B}={{C}}^{{m}}\to {C}\parallel 2{B}\right)$
101 45 100 mpd ${⊢}\left(\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\wedge {{C}}^{{D}}=\left({A}+{B}\right)\left({A}-{B}\right)\right)\to {C}\parallel 2{B}$
102 101 ex ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\to \left({{C}}^{{D}}=\left({A}+{B}\right)\left({A}-{B}\right)\to {C}\parallel 2{B}\right)$
103 8 102 sylbid ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\wedge {B}+1<{A}\right)\wedge \left({C}\in ℙ\wedge {D}\in {ℕ}_{0}\right)\right)\to \left({{C}}^{{D}}={{A}}^{2}-{{B}}^{2}\to {C}\parallel 2{B}\right)$