Proof of Theorem goldbachthlem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fmtnonn 47518 | . . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (FermatNo‘𝑁)
∈ ℕ) | 
| 2 | 1 | nnzd 12640 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ (FermatNo‘𝑁)
∈ ℤ) | 
| 3 |  | fmtnonn 47518 | . . . . . 6
⊢ (𝑀 ∈ ℕ0
→ (FermatNo‘𝑀)
∈ ℕ) | 
| 4 | 3 | nnzd 12640 | . . . . 5
⊢ (𝑀 ∈ ℕ0
→ (FermatNo‘𝑀)
∈ ℤ) | 
| 5 | 2, 4 | anim12ci 614 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → ((FermatNo‘𝑀) ∈ ℤ ∧ (FermatNo‘𝑁) ∈
ℤ)) | 
| 6 | 5 | 3adant3 1133 | . . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
((FermatNo‘𝑀) ∈
ℤ ∧ (FermatNo‘𝑁) ∈ ℤ)) | 
| 7 |  | gcddvds 16540 | . . 3
⊢
(((FermatNo‘𝑀)
∈ ℤ ∧ (FermatNo‘𝑁) ∈ ℤ) →
(((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∥
(FermatNo‘𝑀) ∧
((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∥
(FermatNo‘𝑁))) | 
| 8 | 6, 7 | syl 17 | . 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
(((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∥
(FermatNo‘𝑀) ∧
((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∥
(FermatNo‘𝑁))) | 
| 9 |  | goldbachthlem1 47532 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
(FermatNo‘𝑀) ∥
((FermatNo‘𝑁) −
2)) | 
| 10 |  | gcdcl 16543 | . . . . . . 7
⊢
(((FermatNo‘𝑀)
∈ ℤ ∧ (FermatNo‘𝑁) ∈ ℤ) →
((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∈
ℕ0) | 
| 11 | 6, 10 | syl 17 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∈
ℕ0) | 
| 12 | 11 | nn0zd 12639 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∈
ℤ) | 
| 13 | 4 | 3ad2ant2 1135 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
(FermatNo‘𝑀) ∈
ℤ) | 
| 14 |  | 2z 12649 | . . . . . . . 8
⊢ 2 ∈
ℤ | 
| 15 | 14 | a1i 11 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 2 ∈ ℤ) | 
| 16 | 2, 15 | zsubcld 12727 | . . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ((FermatNo‘𝑁)
− 2) ∈ ℤ) | 
| 17 | 16 | 3ad2ant1 1134 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
((FermatNo‘𝑁) −
2) ∈ ℤ) | 
| 18 |  | dvdstr 16331 | . . . . 5
⊢
((((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) ∈ ℤ ∧
(FermatNo‘𝑀) ∈
ℤ ∧ ((FermatNo‘𝑁) − 2) ∈ ℤ) →
((((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∥
(FermatNo‘𝑀) ∧
(FermatNo‘𝑀) ∥
((FermatNo‘𝑁) −
2)) → ((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) ∥ ((FermatNo‘𝑁) − 2))) | 
| 19 | 12, 13, 17, 18 | syl3anc 1373 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
((((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∥
(FermatNo‘𝑀) ∧
(FermatNo‘𝑀) ∥
((FermatNo‘𝑁) −
2)) → ((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) ∥ ((FermatNo‘𝑁) − 2))) | 
| 20 | 9, 19 | mpan2d 694 | . . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
(((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∥
(FermatNo‘𝑀) →
((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∥
((FermatNo‘𝑁) −
2))) | 
| 21 | 2 | 3ad2ant1 1134 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
(FermatNo‘𝑁) ∈
ℤ) | 
| 22 |  | dvds2sub 16328 | . . . . . 6
⊢
((((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 1373 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
((((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∥
(FermatNo‘𝑁) ∧
((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∥
((FermatNo‘𝑁) −
2)) → ((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) ∥ ((FermatNo‘𝑁) − ((FermatNo‘𝑁) − 2)))) | 
| 24 | 23 | ancomsd 465 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
((((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∥
((FermatNo‘𝑁) −
2) ∧ ((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) ∥ (FermatNo‘𝑁)) → ((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) ∥ ((FermatNo‘𝑁) − ((FermatNo‘𝑁) − 2)))) | 
| 25 | 1 | nncnd 12282 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (FermatNo‘𝑁)
∈ ℂ) | 
| 26 | 25 | 3ad2ant1 1134 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
(FermatNo‘𝑁) ∈
ℂ) | 
| 27 |  | 2cnd 12344 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) → 2 ∈
ℂ) | 
| 28 | 26, 27 | nncand 11625 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
((FermatNo‘𝑁) −
((FermatNo‘𝑁) −
2)) = 2) | 
| 29 | 28 | breq2d 5155 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
(((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∥
((FermatNo‘𝑁) −
((FermatNo‘𝑁) −
2)) ↔ ((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) ∥ 2)) | 
| 30 |  | 2prm 16729 | . . . . . . 7
⊢ 2 ∈
ℙ | 
| 31 | 1, 3 | anim12ci 614 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → ((FermatNo‘𝑀) ∈ ℕ ∧ (FermatNo‘𝑁) ∈
ℕ)) | 
| 32 | 31 | 3adant3 1133 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
((FermatNo‘𝑀) ∈
ℕ ∧ (FermatNo‘𝑁) ∈ ℕ)) | 
| 33 |  | gcdnncl 16544 | . . . . . . . 8
⊢
(((FermatNo‘𝑀)
∈ ℕ ∧ (FermatNo‘𝑁) ∈ ℕ) →
((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∈
ℕ) | 
| 34 | 32, 33 | syl 17 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∈
ℕ) | 
| 35 |  | dvdsprime 16724 | . . . . . . 7
⊢ ((2
∈ ℙ ∧ ((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) ∈ ℕ) →
(((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∥
2 ↔ (((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) = 2 ∨ ((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) = 1))) | 
| 36 | 30, 34, 35 | sylancr 587 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
(((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∥
2 ↔ (((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) = 2 ∨ ((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) = 1))) | 
| 37 | 5, 7 | syl 17 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) ∥ (FermatNo‘𝑀) ∧ ((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) ∥ (FermatNo‘𝑁))) | 
| 38 |  | breq1 5146 | . . . . . . . . . . . . . 14
⊢
(((FermatNo‘𝑀)
gcd (FermatNo‘𝑁)) = 2
→ (((FermatNo‘𝑀)
gcd (FermatNo‘𝑁))
∥ (FermatNo‘𝑁)
↔ 2 ∥ (FermatNo‘𝑁))) | 
| 39 | 38 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ ((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) = 2) → (((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) ∥ (FermatNo‘𝑁) ↔ 2 ∥
(FermatNo‘𝑁))) | 
| 40 |  | fmtnoodd 47520 | . . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ ¬ 2 ∥ (FermatNo‘𝑁)) | 
| 41 | 40 | pm2.21d 121 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (2 ∥ (FermatNo‘𝑁) → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1)) | 
| 42 | 41 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ ((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) = 2) → (2 ∥
(FermatNo‘𝑁) →
((FermatNo‘𝑁) gcd
(FermatNo‘𝑀)) =
1)) | 
| 43 | 39, 42 | sylbid 240 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ ((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) = 2) → (((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) ∥ (FermatNo‘𝑁) → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1)) | 
| 44 | 43 | ex 412 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) = 2 → (((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) ∥ (FermatNo‘𝑁) → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1))) | 
| 45 | 44 | com23 86 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) ∥ (FermatNo‘𝑁) → (((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) = 2 → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1))) | 
| 46 | 45 | adantld 490 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → ((((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) ∥ (FermatNo‘𝑀) ∧ ((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) ∥ (FermatNo‘𝑁)) → (((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) = 2 →
((FermatNo‘𝑁) gcd
(FermatNo‘𝑀)) =
1))) | 
| 47 | 37, 46 | mpd 15 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) = 2 → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1)) | 
| 48 | 47 | 3adant3 1133 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
(((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) = 2
→ ((FermatNo‘𝑁)
gcd (FermatNo‘𝑀)) =
1)) | 
| 49 |  | gcdcom 16550 | . . . . . . . . . 10
⊢
(((FermatNo‘𝑀)
∈ ℤ ∧ (FermatNo‘𝑁) ∈ ℤ) →
((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) =
((FermatNo‘𝑁) gcd
(FermatNo‘𝑀))) | 
| 50 | 6, 49 | syl 17 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) =
((FermatNo‘𝑁) gcd
(FermatNo‘𝑀))) | 
| 51 | 50 | eqeq1d 2739 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
(((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) = 1
↔ ((FermatNo‘𝑁)
gcd (FermatNo‘𝑀)) =
1)) | 
| 52 | 51 | biimpd 229 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
(((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) = 1
→ ((FermatNo‘𝑁)
gcd (FermatNo‘𝑀)) =
1)) | 
| 53 | 48, 52 | jaod 860 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
((((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) = 2
∨ ((FermatNo‘𝑀)
gcd (FermatNo‘𝑁)) =
1) → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1)) | 
| 54 | 36, 53 | sylbid 240 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
(((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∥
2 → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1)) | 
| 55 | 29, 54 | sylbid 240 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
(((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∥
((FermatNo‘𝑁) −
((FermatNo‘𝑁) −
2)) → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1)) | 
| 56 | 24, 55 | syld 47 | . . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
((((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∥
((FermatNo‘𝑁) −
2) ∧ ((FermatNo‘𝑀) gcd (FermatNo‘𝑁)) ∥ (FermatNo‘𝑁)) → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1)) | 
| 57 | 20, 56 | syland 603 | . 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
((((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∥
(FermatNo‘𝑀) ∧
((FermatNo‘𝑀) gcd
(FermatNo‘𝑁)) ∥
(FermatNo‘𝑁)) →
((FermatNo‘𝑁) gcd
(FermatNo‘𝑀)) =
1)) | 
| 58 | 8, 57 | mpd 15 | 1
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
< 𝑁) →
((FermatNo‘𝑁) gcd
(FermatNo‘𝑀)) =
1) |