| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fmtnorn 47526 | . 2
⊢ (𝐹 ∈ ran FermatNo ↔
∃𝑛 ∈
ℕ0 (FermatNo‘𝑛) = 𝐹) | 
| 2 |  | fmtnorn 47526 | . 2
⊢ (𝐺 ∈ ran FermatNo ↔
∃𝑚 ∈
ℕ0 (FermatNo‘𝑚) = 𝐺) | 
| 3 |  | 2a1 28 | . . . . . . . 8
⊢ (𝐹 = 𝐺 → ((FermatNo‘𝑛) = 𝐹 → ((𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐹 = 𝐺))) | 
| 4 | 3 | 2a1d 26 | . . . . . . 7
⊢ (𝐹 = 𝐺 → ((𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
→ ((FermatNo‘𝑚)
= 𝐺 →
((FermatNo‘𝑛) = 𝐹 → ((𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐹 = 𝐺))))) | 
| 5 |  | fmtnonn 47523 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ (FermatNo‘𝑛)
∈ ℕ) | 
| 6 | 5 | ad2antrl 728 | . . . . . . . . . . 11
⊢ ((¬
𝐹 = 𝐺 ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0))
→ (FermatNo‘𝑛)
∈ ℕ) | 
| 7 | 6 | adantr 480 | . . . . . . . . . 10
⊢ (((¬
𝐹 = 𝐺 ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0))
∧ ((FermatNo‘𝑚) =
𝐺 ∧
(FermatNo‘𝑛) = 𝐹)) → (FermatNo‘𝑛) ∈
ℕ) | 
| 8 |  | eleq1 2828 | . . . . . . . . . . 11
⊢
((FermatNo‘𝑛)
= 𝐹 →
((FermatNo‘𝑛) ∈
ℕ ↔ 𝐹 ∈
ℕ)) | 
| 9 | 8 | ad2antll 729 | . . . . . . . . . 10
⊢ (((¬
𝐹 = 𝐺 ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0))
∧ ((FermatNo‘𝑚) =
𝐺 ∧
(FermatNo‘𝑛) = 𝐹)) → ((FermatNo‘𝑛) ∈ ℕ ↔ 𝐹 ∈
ℕ)) | 
| 10 | 7, 9 | mpbid 232 | . . . . . . . . 9
⊢ (((¬
𝐹 = 𝐺 ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0))
∧ ((FermatNo‘𝑚) =
𝐺 ∧
(FermatNo‘𝑛) = 𝐹)) → 𝐹 ∈ ℕ) | 
| 11 |  | fmtnonn 47523 | . . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ0
→ (FermatNo‘𝑚)
∈ ℕ) | 
| 12 | 11 | ad2antll 729 | . . . . . . . . . . 11
⊢ ((¬
𝐹 = 𝐺 ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0))
→ (FermatNo‘𝑚)
∈ ℕ) | 
| 13 | 12 | adantr 480 | . . . . . . . . . 10
⊢ (((¬
𝐹 = 𝐺 ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0))
∧ ((FermatNo‘𝑚) =
𝐺 ∧
(FermatNo‘𝑛) = 𝐹)) → (FermatNo‘𝑚) ∈
ℕ) | 
| 14 |  | eleq1 2828 | . . . . . . . . . . 11
⊢
((FermatNo‘𝑚)
= 𝐺 →
((FermatNo‘𝑚) ∈
ℕ ↔ 𝐺 ∈
ℕ)) | 
| 15 | 14 | ad2antrl 728 | . . . . . . . . . 10
⊢ (((¬
𝐹 = 𝐺 ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0))
∧ ((FermatNo‘𝑚) =
𝐺 ∧
(FermatNo‘𝑛) = 𝐹)) → ((FermatNo‘𝑚) ∈ ℕ ↔ 𝐺 ∈
ℕ)) | 
| 16 | 13, 15 | mpbid 232 | . . . . . . . . 9
⊢ (((¬
𝐹 = 𝐺 ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0))
∧ ((FermatNo‘𝑚) =
𝐺 ∧
(FermatNo‘𝑛) = 𝐹)) → 𝐺 ∈ ℕ) | 
| 17 |  | simpll 766 | . . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) ∧ ¬ (FermatNo‘𝑛) = (FermatNo‘𝑚)) → 𝑛 ∈ ℕ0) | 
| 18 |  | simplr 768 | . . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) ∧ ¬ (FermatNo‘𝑛) = (FermatNo‘𝑚)) → 𝑚 ∈ ℕ0) | 
| 19 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑚 → (FermatNo‘𝑛) = (FermatNo‘𝑚)) | 
| 20 | 19 | con3i 154 | . . . . . . . . . . . . . . . . 17
⊢ (¬
(FermatNo‘𝑛) =
(FermatNo‘𝑚) →
¬ 𝑛 = 𝑚) | 
| 21 | 20 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) ∧ ¬ (FermatNo‘𝑛) = (FermatNo‘𝑚)) → ¬ 𝑛 = 𝑚) | 
| 22 | 21 | neqned 2946 | . . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) ∧ ¬ (FermatNo‘𝑛) = (FermatNo‘𝑚)) → 𝑛 ≠ 𝑚) | 
| 23 |  | goldbachth 47539 | . . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℕ0
∧ 𝑚 ∈
ℕ0 ∧ 𝑛
≠ 𝑚) →
((FermatNo‘𝑛) gcd
(FermatNo‘𝑚)) =
1) | 
| 24 | 17, 18, 22, 23 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) ∧ ¬ (FermatNo‘𝑛) = (FermatNo‘𝑚)) → ((FermatNo‘𝑛) gcd (FermatNo‘𝑚)) = 1) | 
| 25 | 24 | ex 412 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) → (¬ (FermatNo‘𝑛) = (FermatNo‘𝑚) → ((FermatNo‘𝑛) gcd (FermatNo‘𝑚)) = 1)) | 
| 26 |  | eqeq12 2753 | . . . . . . . . . . . . . . . 16
⊢
(((FermatNo‘𝑛)
= 𝐹 ∧
(FermatNo‘𝑚) = 𝐺) → ((FermatNo‘𝑛) = (FermatNo‘𝑚) ↔ 𝐹 = 𝐺)) | 
| 27 | 26 | notbid 318 | . . . . . . . . . . . . . . 15
⊢
(((FermatNo‘𝑛)
= 𝐹 ∧
(FermatNo‘𝑚) = 𝐺) → (¬
(FermatNo‘𝑛) =
(FermatNo‘𝑚) ↔
¬ 𝐹 = 𝐺)) | 
| 28 |  | oveq12 7441 | . . . . . . . . . . . . . . . 16
⊢
(((FermatNo‘𝑛)
= 𝐹 ∧
(FermatNo‘𝑚) = 𝐺) → ((FermatNo‘𝑛) gcd (FermatNo‘𝑚)) = (𝐹 gcd 𝐺)) | 
| 29 | 28 | eqeq1d 2738 | . . . . . . . . . . . . . . 15
⊢
(((FermatNo‘𝑛)
= 𝐹 ∧
(FermatNo‘𝑚) = 𝐺) → (((FermatNo‘𝑛) gcd (FermatNo‘𝑚)) = 1 ↔ (𝐹 gcd 𝐺) = 1)) | 
| 30 | 27, 29 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢
(((FermatNo‘𝑛)
= 𝐹 ∧
(FermatNo‘𝑚) = 𝐺) → ((¬
(FermatNo‘𝑛) =
(FermatNo‘𝑚) →
((FermatNo‘𝑛) gcd
(FermatNo‘𝑚)) = 1)
↔ (¬ 𝐹 = 𝐺 → (𝐹 gcd 𝐺) = 1))) | 
| 31 | 30 | ancoms 458 | . . . . . . . . . . . . 13
⊢
(((FermatNo‘𝑚)
= 𝐺 ∧
(FermatNo‘𝑛) = 𝐹) → ((¬
(FermatNo‘𝑛) =
(FermatNo‘𝑚) →
((FermatNo‘𝑛) gcd
(FermatNo‘𝑚)) = 1)
↔ (¬ 𝐹 = 𝐺 → (𝐹 gcd 𝐺) = 1))) | 
| 32 | 25, 31 | syl5ibcom 245 | . . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) → (((FermatNo‘𝑚) = 𝐺 ∧ (FermatNo‘𝑛) = 𝐹) → (¬ 𝐹 = 𝐺 → (𝐹 gcd 𝐺) = 1))) | 
| 33 | 32 | com23 86 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) → (¬ 𝐹 = 𝐺 → (((FermatNo‘𝑚) = 𝐺 ∧ (FermatNo‘𝑛) = 𝐹) → (𝐹 gcd 𝐺) = 1))) | 
| 34 | 33 | impcom 407 | . . . . . . . . . 10
⊢ ((¬
𝐹 = 𝐺 ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0))
→ (((FermatNo‘𝑚)
= 𝐺 ∧
(FermatNo‘𝑛) = 𝐹) → (𝐹 gcd 𝐺) = 1)) | 
| 35 | 34 | imp 406 | . . . . . . . . 9
⊢ (((¬
𝐹 = 𝐺 ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0))
∧ ((FermatNo‘𝑚) =
𝐺 ∧
(FermatNo‘𝑛) = 𝐹)) → (𝐹 gcd 𝐺) = 1) | 
| 36 |  | prmnn 16712 | . . . . . . . . . . . 12
⊢ (𝐼 ∈ ℙ → 𝐼 ∈
ℕ) | 
| 37 |  | coprmdvds1 16690 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ ℕ ∧ 𝐺 ∈ ℕ ∧ (𝐹 gcd 𝐺) = 1) → ((𝐼 ∈ ℕ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐼 = 1)) | 
| 38 | 37 | imp 406 | . . . . . . . . . . . 12
⊢ (((𝐹 ∈ ℕ ∧ 𝐺 ∈ ℕ ∧ (𝐹 gcd 𝐺) = 1) ∧ (𝐼 ∈ ℕ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺)) → 𝐼 = 1) | 
| 39 | 36, 38 | syl3anr1 1417 | . . . . . . . . . . 11
⊢ (((𝐹 ∈ ℕ ∧ 𝐺 ∈ ℕ ∧ (𝐹 gcd 𝐺) = 1) ∧ (𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺)) → 𝐼 = 1) | 
| 40 |  | eleq1 2828 | . . . . . . . . . . . . . . . 16
⊢ (𝐼 = 1 → (𝐼 ∈ ℙ ↔ 1 ∈
ℙ)) | 
| 41 |  | 1nprm 16717 | . . . . . . . . . . . . . . . . 17
⊢  ¬ 1
∈ ℙ | 
| 42 | 41 | pm2.21i 119 | . . . . . . . . . . . . . . . 16
⊢ (1 ∈
ℙ → 𝐹 = 𝐺) | 
| 43 | 40, 42 | biimtrdi 253 | . . . . . . . . . . . . . . 15
⊢ (𝐼 = 1 → (𝐼 ∈ ℙ → 𝐹 = 𝐺)) | 
| 44 | 43 | com12 32 | . . . . . . . . . . . . . 14
⊢ (𝐼 ∈ ℙ → (𝐼 = 1 → 𝐹 = 𝐺)) | 
| 45 | 44 | a1d 25 | . . . . . . . . . . . . 13
⊢ (𝐼 ∈ ℙ → ((𝐹 ∈ ℕ ∧ 𝐺 ∈ ℕ ∧ (𝐹 gcd 𝐺) = 1) → (𝐼 = 1 → 𝐹 = 𝐺))) | 
| 46 | 45 | 3ad2ant1 1133 | . . . . . . . . . . . 12
⊢ ((𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → ((𝐹 ∈ ℕ ∧ 𝐺 ∈ ℕ ∧ (𝐹 gcd 𝐺) = 1) → (𝐼 = 1 → 𝐹 = 𝐺))) | 
| 47 | 46 | impcom 407 | . . . . . . . . . . 11
⊢ (((𝐹 ∈ ℕ ∧ 𝐺 ∈ ℕ ∧ (𝐹 gcd 𝐺) = 1) ∧ (𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺)) → (𝐼 = 1 → 𝐹 = 𝐺)) | 
| 48 | 39, 47 | mpd 15 | . . . . . . . . . 10
⊢ (((𝐹 ∈ ℕ ∧ 𝐺 ∈ ℕ ∧ (𝐹 gcd 𝐺) = 1) ∧ (𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺)) → 𝐹 = 𝐺) | 
| 49 | 48 | ex 412 | . . . . . . . . 9
⊢ ((𝐹 ∈ ℕ ∧ 𝐺 ∈ ℕ ∧ (𝐹 gcd 𝐺) = 1) → ((𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐹 = 𝐺)) | 
| 50 | 10, 16, 35, 49 | syl3anc 1372 | . . . . . . . 8
⊢ (((¬
𝐹 = 𝐺 ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0))
∧ ((FermatNo‘𝑚) =
𝐺 ∧
(FermatNo‘𝑛) = 𝐹)) → ((𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐹 = 𝐺)) | 
| 51 | 50 | exp43 436 | . . . . . . 7
⊢ (¬
𝐹 = 𝐺 → ((𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
→ ((FermatNo‘𝑚)
= 𝐺 →
((FermatNo‘𝑛) = 𝐹 → ((𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐹 = 𝐺))))) | 
| 52 | 4, 51 | pm2.61i 182 | . . . . . 6
⊢ ((𝑛 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) → ((FermatNo‘𝑚) = 𝐺 → ((FermatNo‘𝑛) = 𝐹 → ((𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐹 = 𝐺)))) | 
| 53 | 52 | rexlimdva 3154 | . . . . 5
⊢ (𝑛 ∈ ℕ0
→ (∃𝑚 ∈
ℕ0 (FermatNo‘𝑚) = 𝐺 → ((FermatNo‘𝑛) = 𝐹 → ((𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐹 = 𝐺)))) | 
| 54 | 53 | com23 86 | . . . 4
⊢ (𝑛 ∈ ℕ0
→ ((FermatNo‘𝑛)
= 𝐹 → (∃𝑚 ∈ ℕ0
(FermatNo‘𝑚) = 𝐺 → ((𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐹 = 𝐺)))) | 
| 55 | 54 | rexlimiv 3147 | . . 3
⊢
(∃𝑛 ∈
ℕ0 (FermatNo‘𝑛) = 𝐹 → (∃𝑚 ∈ ℕ0
(FermatNo‘𝑚) = 𝐺 → ((𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐹 = 𝐺))) | 
| 56 | 55 | imp 406 | . 2
⊢
((∃𝑛 ∈
ℕ0 (FermatNo‘𝑛) = 𝐹 ∧ ∃𝑚 ∈ ℕ0
(FermatNo‘𝑚) = 𝐺) → ((𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐹 = 𝐺)) | 
| 57 | 1, 2, 56 | syl2anb 598 | 1
⊢ ((𝐹 ∈ ran FermatNo ∧ 𝐺 ∈ ran FermatNo) →
((𝐼 ∈ ℙ ∧
𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐹 = 𝐺)) |