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 )