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 ⊢A∈ℕ0∧B∈ℕ0∧B+1<A∧C∈ℙ∧D∈ℕ0→CD=A2−B2→C∥2⁢B

Proof

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