Metamath Proof Explorer


Theorem goldbachthlem2

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

Ref Expression
Assertion goldbachthlem2 ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 )

Proof

Step Hyp Ref Expression
1 fmtnonn ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) ∈ ℕ )
2 1 nnzd ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) ∈ ℤ )
3 fmtnonn ( 𝑀 ∈ ℕ0 → ( FermatNo ‘ 𝑀 ) ∈ ℕ )
4 3 nnzd ( 𝑀 ∈ ℕ0 → ( FermatNo ‘ 𝑀 ) ∈ ℤ )
5 2 4 anim12ci ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0 ) → ( ( FermatNo ‘ 𝑀 ) ∈ ℤ ∧ ( FermatNo ‘ 𝑁 ) ∈ ℤ ) )
6 5 3adant3 ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( FermatNo ‘ 𝑀 ) ∈ ℤ ∧ ( FermatNo ‘ 𝑁 ) ∈ ℤ ) )
7 gcddvds ( ( ( FermatNo ‘ 𝑀 ) ∈ ℤ ∧ ( FermatNo ‘ 𝑁 ) ∈ ℤ ) → ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑀 ) ∧ ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑁 ) ) )
8 6 7 syl ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑀 ) ∧ ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑁 ) ) )
9 goldbachthlem1 ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( FermatNo ‘ 𝑀 ) ∥ ( ( FermatNo ‘ 𝑁 ) − 2 ) )
10 gcdcl ( ( ( FermatNo ‘ 𝑀 ) ∈ ℤ ∧ ( FermatNo ‘ 𝑁 ) ∈ ℤ ) → ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∈ ℕ0 )
11 6 10 syl ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∈ ℕ0 )
12 11 nn0zd ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∈ ℤ )
13 4 3ad2ant2 ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( FermatNo ‘ 𝑀 ) ∈ ℤ )
14 2z 2 ∈ ℤ
15 14 a1i ( 𝑁 ∈ ℕ0 → 2 ∈ ℤ )
16 2 15 zsubcld ( 𝑁 ∈ ℕ0 → ( ( FermatNo ‘ 𝑁 ) − 2 ) ∈ ℤ )
17 16 3ad2ant1 ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( FermatNo ‘ 𝑁 ) − 2 ) ∈ ℤ )
18 dvdstr ( ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∈ ℤ ∧ ( FermatNo ‘ 𝑀 ) ∈ ℤ ∧ ( ( FermatNo ‘ 𝑁 ) − 2 ) ∈ ℤ ) → ( ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑀 ) ∧ ( FermatNo ‘ 𝑀 ) ∥ ( ( FermatNo ‘ 𝑁 ) − 2 ) ) → ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( ( FermatNo ‘ 𝑁 ) − 2 ) ) )
19 12 13 17 18 syl3anc ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑀 ) ∧ ( FermatNo ‘ 𝑀 ) ∥ ( ( FermatNo ‘ 𝑁 ) − 2 ) ) → ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( ( FermatNo ‘ 𝑁 ) − 2 ) ) )
20 9 19 mpan2d ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑀 ) → ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( ( FermatNo ‘ 𝑁 ) − 2 ) ) )
21 2 3ad2ant1 ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( FermatNo ‘ 𝑁 ) ∈ ℤ )
22 dvds2sub ( ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∈ ℤ ∧ ( FermatNo ‘ 𝑁 ) ∈ ℤ ∧ ( ( FermatNo ‘ 𝑁 ) − 2 ) ∈ ℤ ) → ( ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑁 ) ∧ ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( ( FermatNo ‘ 𝑁 ) − 2 ) ) → ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( ( FermatNo ‘ 𝑁 ) − ( ( FermatNo ‘ 𝑁 ) − 2 ) ) ) )
23 12 21 17 22 syl3anc ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑁 ) ∧ ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( ( FermatNo ‘ 𝑁 ) − 2 ) ) → ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( ( FermatNo ‘ 𝑁 ) − ( ( FermatNo ‘ 𝑁 ) − 2 ) ) ) )
24 23 ancomsd ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( ( FermatNo ‘ 𝑁 ) − 2 ) ∧ ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑁 ) ) → ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( ( FermatNo ‘ 𝑁 ) − ( ( FermatNo ‘ 𝑁 ) − 2 ) ) ) )
25 1 nncnd ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) ∈ ℂ )
26 25 3ad2ant1 ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( FermatNo ‘ 𝑁 ) ∈ ℂ )
27 2cnd ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → 2 ∈ ℂ )
28 26 27 nncand ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( FermatNo ‘ 𝑁 ) − ( ( FermatNo ‘ 𝑁 ) − 2 ) ) = 2 )
29 28 breq2d ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( ( FermatNo ‘ 𝑁 ) − ( ( FermatNo ‘ 𝑁 ) − 2 ) ) ↔ ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ 2 ) )
30 2prm 2 ∈ ℙ
31 1 3 anim12ci ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0 ) → ( ( FermatNo ‘ 𝑀 ) ∈ ℕ ∧ ( FermatNo ‘ 𝑁 ) ∈ ℕ ) )
32 31 3adant3 ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( FermatNo ‘ 𝑀 ) ∈ ℕ ∧ ( FermatNo ‘ 𝑁 ) ∈ ℕ ) )
33 gcdnncl ( ( ( FermatNo ‘ 𝑀 ) ∈ ℕ ∧ ( FermatNo ‘ 𝑁 ) ∈ ℕ ) → ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∈ ℕ )
34 32 33 syl ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∈ ℕ )
35 dvdsprime ( ( 2 ∈ ℙ ∧ ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∈ ℕ ) → ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ 2 ↔ ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) = 2 ∨ ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) = 1 ) ) )
36 30 34 35 sylancr ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ 2 ↔ ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) = 2 ∨ ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) = 1 ) ) )
37 5 7 syl ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0 ) → ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑀 ) ∧ ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑁 ) ) )
38 breq1 ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) = 2 → ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑁 ) ↔ 2 ∥ ( FermatNo ‘ 𝑁 ) ) )
39 38 adantl ( ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0 ) ∧ ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) = 2 ) → ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑁 ) ↔ 2 ∥ ( FermatNo ‘ 𝑁 ) ) )
40 fmtnoodd ( 𝑁 ∈ ℕ0 → ¬ 2 ∥ ( FermatNo ‘ 𝑁 ) )
41 40 pm2.21d ( 𝑁 ∈ ℕ0 → ( 2 ∥ ( FermatNo ‘ 𝑁 ) → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) )
42 41 ad2antrr ( ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0 ) ∧ ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) = 2 ) → ( 2 ∥ ( FermatNo ‘ 𝑁 ) → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) )
43 39 42 sylbid ( ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0 ) ∧ ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) = 2 ) → ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑁 ) → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) )
44 43 ex ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0 ) → ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) = 2 → ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑁 ) → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) ) )
45 44 com23 ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0 ) → ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑁 ) → ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) = 2 → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) ) )
46 45 adantld ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0 ) → ( ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑀 ) ∧ ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑁 ) ) → ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) = 2 → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) ) )
47 37 46 mpd ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0 ) → ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) = 2 → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) )
48 47 3adant3 ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) = 2 → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) )
49 gcdcom ( ( ( FermatNo ‘ 𝑀 ) ∈ ℤ ∧ ( FermatNo ‘ 𝑁 ) ∈ ℤ ) → ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) = ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) )
50 6 49 syl ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) = ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) )
51 50 eqeq1d ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) = 1 ↔ ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) )
52 51 biimpd ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) = 1 → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) )
53 48 52 jaod ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) = 2 ∨ ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) = 1 ) → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) )
54 36 53 sylbid ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ 2 → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) )
55 29 54 sylbid ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( ( FermatNo ‘ 𝑁 ) − ( ( FermatNo ‘ 𝑁 ) − 2 ) ) → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) )
56 24 55 syld ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( ( FermatNo ‘ 𝑁 ) − 2 ) ∧ ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑁 ) ) → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) )
57 20 56 syland ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑀 ) ∧ ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) ∥ ( FermatNo ‘ 𝑁 ) ) → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) )
58 8 57 mpd ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 )