Metamath Proof Explorer

Theorem goldbachthlem2

Description: Lemma 2 for goldbachth . (Contributed by AV, 1-Aug-2021)

Ref Expression
Assertion goldbachthlem2 
|- ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 )

Proof

Step Hyp Ref Expression
1 fmtnonn 
 |-  ( N e. NN0 -> ( FermatNo ` N ) e. NN )
2 1 nnzd 
 |-  ( N e. NN0 -> ( FermatNo ` N ) e. ZZ )
3 fmtnonn 
 |-  ( M e. NN0 -> ( FermatNo ` M ) e. NN )
4 3 nnzd 
 |-  ( M e. NN0 -> ( FermatNo ` M ) e. ZZ )
5 2 4 anim12ci 
 |-  ( ( N e. NN0 /\ M e. NN0 ) -> ( ( FermatNo ` M ) e. ZZ /\ ( FermatNo ` N ) e. ZZ ) )
6 5 3adant3 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( FermatNo ` M ) e. ZZ /\ ( FermatNo ` N ) e. ZZ ) )
7 gcddvds 
 |-  ( ( ( FermatNo ` M ) e. ZZ /\ ( FermatNo ` N ) e. ZZ ) -> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` M ) /\ ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` N ) ) )
8 6 7 syl 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` M ) /\ ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` N ) ) )
9 goldbachthlem1 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( FermatNo ` M ) || ( ( FermatNo ` N ) - 2 ) )
10 gcdcl 
 |-  ( ( ( FermatNo ` M ) e. ZZ /\ ( FermatNo ` N ) e. ZZ ) -> ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) e. NN0 )
11 6 10 syl 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) e. NN0 )
12 11 nn0zd 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) e. ZZ )
13 4 3ad2ant2 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( FermatNo ` M ) e. ZZ )
14 2z 
 |-  2 e. ZZ
15 14 a1i 
 |-  ( N e. NN0 -> 2 e. ZZ )
16 2 15 zsubcld 
 |-  ( N e. NN0 -> ( ( FermatNo ` N ) - 2 ) e. ZZ )
17 16 3ad2ant1 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( FermatNo ` N ) - 2 ) e. ZZ )
18 dvdstr 
 |-  ( ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) e. ZZ /\ ( FermatNo ` M ) e. ZZ /\ ( ( FermatNo ` N ) - 2 ) e. ZZ ) -> ( ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` M ) /\ ( FermatNo ` M ) || ( ( FermatNo ` N ) - 2 ) ) -> ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( ( FermatNo ` N ) - 2 ) ) )
19 12 13 17 18 syl3anc 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` M ) /\ ( FermatNo ` M ) || ( ( FermatNo ` N ) - 2 ) ) -> ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( ( FermatNo ` N ) - 2 ) ) )
20 9 19 mpan2d 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` M ) -> ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( ( FermatNo ` N ) - 2 ) ) )
21 2 3ad2ant1 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( FermatNo ` N ) e. ZZ )
22 dvds2sub 
 |-  ( ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) e. ZZ /\ ( FermatNo ` N ) e. ZZ /\ ( ( FermatNo ` N ) - 2 ) e. ZZ ) -> ( ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` N ) /\ ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( ( FermatNo ` N ) - 2 ) ) -> ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( ( FermatNo ` N ) - ( ( FermatNo ` N ) - 2 ) ) ) )
23 12 21 17 22 syl3anc 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` N ) /\ ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( ( FermatNo ` N ) - 2 ) ) -> ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( ( FermatNo ` N ) - ( ( FermatNo ` N ) - 2 ) ) ) )
24 23 ancomsd 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( ( FermatNo ` N ) - 2 ) /\ ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` N ) ) -> ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( ( FermatNo ` N ) - ( ( FermatNo ` N ) - 2 ) ) ) )
25 1 nncnd 
 |-  ( N e. NN0 -> ( FermatNo ` N ) e. CC )
26 25 3ad2ant1 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( FermatNo ` N ) e. CC )
27 2cnd 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> 2 e. CC )
28 26 27 nncand 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( FermatNo ` N ) - ( ( FermatNo ` N ) - 2 ) ) = 2 )
29 28 breq2d 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( ( FermatNo ` N ) - ( ( FermatNo ` N ) - 2 ) ) <-> ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || 2 ) )
30 2prm 
 |-  2 e. Prime
31 1 3 anim12ci 
 |-  ( ( N e. NN0 /\ M e. NN0 ) -> ( ( FermatNo ` M ) e. NN /\ ( FermatNo ` N ) e. NN ) )
32 31 3adant3 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( FermatNo ` M ) e. NN /\ ( FermatNo ` N ) e. NN ) )
33 gcdnncl 
 |-  ( ( ( FermatNo ` M ) e. NN /\ ( FermatNo ` N ) e. NN ) -> ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) e. NN )
34 32 33 syl 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) e. NN )
35 dvdsprime 
 |-  ( ( 2 e. Prime /\ ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) e. NN ) -> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || 2 <-> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) = 2 \/ ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) = 1 ) ) )
36 30 34 35 sylancr 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || 2 <-> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) = 2 \/ ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) = 1 ) ) )
37 5 7 syl 
 |-  ( ( N e. NN0 /\ M e. NN0 ) -> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` M ) /\ ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` N ) ) )
38 breq1 
 |-  ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) = 2 -> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` N ) <-> 2 || ( FermatNo ` N ) ) )
39 38 adantl 
 |-  ( ( ( N e. NN0 /\ M e. NN0 ) /\ ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) = 2 ) -> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` N ) <-> 2 || ( FermatNo ` N ) ) )
40 fmtnoodd 
 |-  ( N e. NN0 -> -. 2 || ( FermatNo ` N ) )
41 40 pm2.21d 
 |-  ( N e. NN0 -> ( 2 || ( FermatNo ` N ) -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) )
42 41 ad2antrr 
 |-  ( ( ( N e. NN0 /\ M e. NN0 ) /\ ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) = 2 ) -> ( 2 || ( FermatNo ` N ) -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) )
43 39 42 sylbid 
 |-  ( ( ( N e. NN0 /\ M e. NN0 ) /\ ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) = 2 ) -> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` N ) -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) )
44 43 ex 
 |-  ( ( N e. NN0 /\ M e. NN0 ) -> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) = 2 -> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` N ) -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) ) )
45 44 com23 
 |-  ( ( N e. NN0 /\ M e. NN0 ) -> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` N ) -> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) = 2 -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) ) )
46 45 adantld 
 |-  ( ( N e. NN0 /\ M e. NN0 ) -> ( ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` M ) /\ ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` N ) ) -> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) = 2 -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) ) )
47 37 46 mpd 
 |-  ( ( N e. NN0 /\ M e. NN0 ) -> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) = 2 -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) )
48 47 3adant3 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) = 2 -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) )
49 gcdcom 
 |-  ( ( ( FermatNo ` M ) e. ZZ /\ ( FermatNo ` N ) e. ZZ ) -> ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) = ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) )
50 6 49 syl 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) = ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) )
51 50 eqeq1d 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) = 1 <-> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) )
52 51 biimpd 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) = 1 -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) )
53 48 52 jaod 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) = 2 \/ ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) = 1 ) -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) )
54 36 53 sylbid 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || 2 -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) )
55 29 54 sylbid 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( ( FermatNo ` N ) - ( ( FermatNo ` N ) - 2 ) ) -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) )
56 24 55 syld 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( ( FermatNo ` N ) - 2 ) /\ ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` N ) ) -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) )
57 20 56 syland 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` M ) /\ ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) || ( FermatNo ` N ) ) -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) )
58 8 57 mpd 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 )