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 e. NN0 /\ B e. NN0 /\ ( B + 1 ) < A ) /\ ( C e. Prime /\ D e. NN0 ) ) -> ( ( C ^ D ) = ( ( A ^ 2 ) - ( B ^ 2 ) ) -> C || ( 2 x. B ) ) )

Proof

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