Proof of Theorem nfermltl2rev
| Step | Hyp | Ref
| Expression |
| 1 | | decex 12737 |
. . 3
⊢ ;;341 ∈ V |
| 2 | | eleq1 2829 |
. . . 4
⊢ (𝑝 = ;;341
→ (𝑝 ∈
(ℤ≥‘3) ↔ ;;341
∈ (ℤ≥‘3))) |
| 3 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑝 = ;;341
→ (2↑𝑝) =
(2↑;;341)) |
| 4 | | id 22 |
. . . . . . . 8
⊢ (𝑝 = ;;341
→ 𝑝 = ;;341) |
| 5 | 3, 4 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑝 = ;;341
→ ((2↑𝑝) mod
𝑝) = ((2↑;;341) mod ;;341)) |
| 6 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑝 = ;;341
→ (2 mod 𝑝) = (2 mod
;;341)) |
| 7 | 5, 6 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑝 = ;;341
→ (((2↑𝑝) mod
𝑝) = (2 mod 𝑝) ↔ ((2↑;;341) mod ;;341) =
(2 mod ;;341))) |
| 8 | | eleq1 2829 |
. . . . . 6
⊢ (𝑝 = ;;341
→ (𝑝 ∈ ℙ
↔ ;;341 ∈ ℙ)) |
| 9 | 7, 8 | imbi12d 344 |
. . . . 5
⊢ (𝑝 = ;;341
→ ((((2↑𝑝) mod
𝑝) = (2 mod 𝑝) → 𝑝 ∈ ℙ) ↔ (((2↑;;341) mod ;;341) =
(2 mod ;;341) → ;;341
∈ ℙ))) |
| 10 | 9 | notbid 318 |
. . . 4
⊢ (𝑝 = ;;341
→ (¬ (((2↑𝑝)
mod 𝑝) = (2 mod 𝑝) → 𝑝 ∈ ℙ) ↔ ¬ (((2↑;;341) mod ;;341) =
(2 mod ;;341) → ;;341
∈ ℙ))) |
| 11 | 2, 10 | anbi12d 632 |
. . 3
⊢ (𝑝 = ;;341
→ ((𝑝 ∈
(ℤ≥‘3) ∧ ¬ (((2↑𝑝) mod 𝑝) = (2 mod 𝑝) → 𝑝 ∈ ℙ)) ↔ (;;341
∈ (ℤ≥‘3) ∧ ¬ (((2↑;;341) mod ;;341) =
(2 mod ;;341) → ;;341
∈ ℙ)))) |
| 12 | | 3z 12650 |
. . . . 5
⊢ 3 ∈
ℤ |
| 13 | | 3nn0 12544 |
. . . . . . . 8
⊢ 3 ∈
ℕ0 |
| 14 | | 4nn0 12545 |
. . . . . . . 8
⊢ 4 ∈
ℕ0 |
| 15 | 13, 14 | deccl 12748 |
. . . . . . 7
⊢ ;34 ∈
ℕ0 |
| 16 | | 1nn0 12542 |
. . . . . . 7
⊢ 1 ∈
ℕ0 |
| 17 | 15, 16 | deccl 12748 |
. . . . . 6
⊢ ;;341 ∈ ℕ0 |
| 18 | 17 | nn0zi 12642 |
. . . . 5
⊢ ;;341 ∈ ℤ |
| 19 | 13 | dec0h 12755 |
. . . . . 6
⊢ 3 = ;03 |
| 20 | | 0nn0 12541 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
| 21 | | 3re 12346 |
. . . . . . . 8
⊢ 3 ∈
ℝ |
| 22 | | 9re 12365 |
. . . . . . . 8
⊢ 9 ∈
ℝ |
| 23 | | 3lt9 12470 |
. . . . . . . 8
⊢ 3 <
9 |
| 24 | 21, 22, 23 | ltleii 11384 |
. . . . . . 7
⊢ 3 ≤
9 |
| 25 | | 3nn 12345 |
. . . . . . . 8
⊢ 3 ∈
ℕ |
| 26 | | 0re 11263 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
| 27 | | 9pos 12379 |
. . . . . . . . 9
⊢ 0 <
9 |
| 28 | 26, 22, 27 | ltleii 11384 |
. . . . . . . 8
⊢ 0 ≤
9 |
| 29 | 25, 14, 20, 28 | decltdi 12772 |
. . . . . . 7
⊢ 0 <
;34 |
| 30 | 20, 15, 13, 16, 24, 29 | decleh 12768 |
. . . . . 6
⊢ ;03 ≤ ;;341 |
| 31 | 19, 30 | eqbrtri 5164 |
. . . . 5
⊢ 3 ≤
;;341 |
| 32 | | eluz2 12884 |
. . . . 5
⊢ (;;341 ∈ (ℤ≥‘3) ↔
(3 ∈ ℤ ∧ ;;341 ∈ ℤ ∧ 3 ≤ ;;341)) |
| 33 | 12, 18, 31, 32 | mpbir3an 1342 |
. . . 4
⊢ ;;341 ∈
(ℤ≥‘3) |
| 34 | | 341fppr2 47721 |
. . . . . . 7
⊢ ;;341 ∈ ( FPPr ‘2) |
| 35 | | fpprwppr 47726 |
. . . . . . 7
⊢ (;;341 ∈ ( FPPr ‘2) → ((2↑;;341) mod ;;341) =
(2 mod ;;341)) |
| 36 | 34, 35 | ax-mp 5 |
. . . . . 6
⊢
((2↑;;341) mod ;;341) =
(2 mod ;;341) |
| 37 | | 11t31e341 47719 |
. . . . . . . 8
⊢ (;11 · ;31) = ;;341 |
| 38 | 37 | eqcomi 2746 |
. . . . . . 7
⊢ ;;341 = (;11 · ;31) |
| 39 | | 2z 12649 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
| 40 | 16, 16 | deccl 12748 |
. . . . . . . . . 10
⊢ ;11 ∈
ℕ0 |
| 41 | 40 | nn0zi 12642 |
. . . . . . . . 9
⊢ ;11 ∈ ℤ |
| 42 | | 2nn0 12543 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
| 43 | 42 | dec0h 12755 |
. . . . . . . . . 10
⊢ 2 = ;02 |
| 44 | | 2re 12340 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
| 45 | | 2lt9 12471 |
. . . . . . . . . . . 12
⊢ 2 <
9 |
| 46 | 44, 22, 45 | ltleii 11384 |
. . . . . . . . . . 11
⊢ 2 ≤
9 |
| 47 | | 0lt1 11785 |
. . . . . . . . . . 11
⊢ 0 <
1 |
| 48 | 20, 16, 42, 16, 46, 47 | decleh 12768 |
. . . . . . . . . 10
⊢ ;02 ≤ ;11 |
| 49 | 43, 48 | eqbrtri 5164 |
. . . . . . . . 9
⊢ 2 ≤
;11 |
| 50 | | eluz2 12884 |
. . . . . . . . 9
⊢ (;11 ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ ;11 ∈ ℤ ∧ 2 ≤ ;11)) |
| 51 | 39, 41, 49, 50 | mpbir3an 1342 |
. . . . . . . 8
⊢ ;11 ∈
(ℤ≥‘2) |
| 52 | 13, 16 | deccl 12748 |
. . . . . . . . . 10
⊢ ;31 ∈
ℕ0 |
| 53 | 52 | nn0zi 12642 |
. . . . . . . . 9
⊢ ;31 ∈ ℤ |
| 54 | | 3pos 12371 |
. . . . . . . . . . 11
⊢ 0 <
3 |
| 55 | 20, 13, 42, 16, 46, 54 | decleh 12768 |
. . . . . . . . . 10
⊢ ;02 ≤ ;31 |
| 56 | 43, 55 | eqbrtri 5164 |
. . . . . . . . 9
⊢ 2 ≤
;31 |
| 57 | | eluz2 12884 |
. . . . . . . . 9
⊢ (;31 ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ ;31 ∈ ℤ ∧ 2 ≤ ;31)) |
| 58 | 39, 53, 56, 57 | mpbir3an 1342 |
. . . . . . . 8
⊢ ;31 ∈
(ℤ≥‘2) |
| 59 | | nprm 16725 |
. . . . . . . 8
⊢ ((;11 ∈
(ℤ≥‘2) ∧ ;31 ∈ (ℤ≥‘2)) →
¬ (;11 · ;31) ∈ ℙ) |
| 60 | 51, 58, 59 | mp2an 692 |
. . . . . . 7
⊢ ¬
(;11 · ;31) ∈ ℙ |
| 61 | 38, 60 | eqneltri 2860 |
. . . . . 6
⊢ ¬
;;341 ∈ ℙ |
| 62 | 36, 61 | pm3.2i 470 |
. . . . 5
⊢
(((2↑;;341) mod ;;341) =
(2 mod ;;341) ∧ ¬ ;;341
∈ ℙ) |
| 63 | | annim 403 |
. . . . 5
⊢
((((2↑;;341) mod ;;341) =
(2 mod ;;341) ∧ ¬ ;;341
∈ ℙ) ↔ ¬ (((2↑;;341)
mod ;;341) = (2 mod ;;341)
→ ;;341 ∈ ℙ)) |
| 64 | 62, 63 | mpbi 230 |
. . . 4
⊢ ¬
(((2↑;;341) mod ;;341) =
(2 mod ;;341) → ;;341
∈ ℙ) |
| 65 | 33, 64 | pm3.2i 470 |
. . 3
⊢ (;;341 ∈ (ℤ≥‘3) ∧
¬ (((2↑;;341) mod ;;341) =
(2 mod ;;341) → ;;341
∈ ℙ)) |
| 66 | 1, 11, 65 | ceqsexv2d 3533 |
. 2
⊢
∃𝑝(𝑝 ∈
(ℤ≥‘3) ∧ ¬ (((2↑𝑝) mod 𝑝) = (2 mod 𝑝) → 𝑝 ∈ ℙ)) |
| 67 | | df-rex 3071 |
. 2
⊢
(∃𝑝 ∈
(ℤ≥‘3) ¬ (((2↑𝑝) mod 𝑝) = (2 mod 𝑝) → 𝑝 ∈ ℙ) ↔ ∃𝑝(𝑝 ∈ (ℤ≥‘3)
∧ ¬ (((2↑𝑝)
mod 𝑝) = (2 mod 𝑝) → 𝑝 ∈ ℙ))) |
| 68 | 66, 67 | mpbir 231 |
1
⊢
∃𝑝 ∈
(ℤ≥‘3) ¬ (((2↑𝑝) mod 𝑝) = (2 mod 𝑝) → 𝑝 ∈ ℙ) |