Proof of Theorem 37prm
| Step | Hyp | Ref
| Expression |
| 1 | | 3nn0 12544 |
. . 3
⊢ 3 ∈
ℕ0 |
| 2 | | 7nn 12358 |
. . 3
⊢ 7 ∈
ℕ |
| 3 | 1, 2 | decnncl 12753 |
. 2
⊢ ;37 ∈ ℕ |
| 4 | | 8nn0 12549 |
. . . 4
⊢ 8 ∈
ℕ0 |
| 5 | | 4nn0 12545 |
. . . 4
⊢ 4 ∈
ℕ0 |
| 6 | 4, 5 | deccl 12748 |
. . 3
⊢ ;84 ∈
ℕ0 |
| 7 | | 7nn0 12548 |
. . 3
⊢ 7 ∈
ℕ0 |
| 8 | | 1nn0 12542 |
. . 3
⊢ 1 ∈
ℕ0 |
| 9 | | 7lt10 12866 |
. . 3
⊢ 7 <
;10 |
| 10 | | 8nn 12361 |
. . . 4
⊢ 8 ∈
ℕ |
| 11 | | 3lt10 12870 |
. . . 4
⊢ 3 <
;10 |
| 12 | 10, 5, 1, 11 | declti 12771 |
. . 3
⊢ 3 <
;84 |
| 13 | 1, 6, 7, 8, 9, 12 | decltc 12762 |
. 2
⊢ ;37 < ;;841 |
| 14 | | 3nn 12345 |
. . 3
⊢ 3 ∈
ℕ |
| 15 | | 1lt10 12872 |
. . 3
⊢ 1 <
;10 |
| 16 | 14, 7, 8, 15 | declti 12771 |
. 2
⊢ 1 <
;37 |
| 17 | | 3t2e6 12432 |
. . 3
⊢ (3
· 2) = 6 |
| 18 | | df-7 12334 |
. . 3
⊢ 7 = (6 +
1) |
| 19 | 1, 1, 17, 18 | dec2dvds 17101 |
. 2
⊢ ¬ 2
∥ ;37 |
| 20 | | 2nn0 12543 |
. . . 4
⊢ 2 ∈
ℕ0 |
| 21 | 8, 20 | deccl 12748 |
. . 3
⊢ ;12 ∈
ℕ0 |
| 22 | | 1nn 12277 |
. . 3
⊢ 1 ∈
ℕ |
| 23 | | 6nn0 12547 |
. . . 4
⊢ 6 ∈
ℕ0 |
| 24 | | 6p1e7 12414 |
. . . 4
⊢ (6 + 1) =
7 |
| 25 | | eqid 2737 |
. . . . 5
⊢ ;12 = ;12 |
| 26 | | 0nn0 12541 |
. . . . 5
⊢ 0 ∈
ℕ0 |
| 27 | | 3cn 12347 |
. . . . . . . 8
⊢ 3 ∈
ℂ |
| 28 | 27 | mulridi 11265 |
. . . . . . 7
⊢ (3
· 1) = 3 |
| 29 | 28 | oveq1i 7441 |
. . . . . 6
⊢ ((3
· 1) + 0) = (3 + 0) |
| 30 | 27 | addridi 11448 |
. . . . . 6
⊢ (3 + 0) =
3 |
| 31 | 29, 30 | eqtri 2765 |
. . . . 5
⊢ ((3
· 1) + 0) = 3 |
| 32 | 23 | dec0h 12755 |
. . . . . 6
⊢ 6 = ;06 |
| 33 | 17, 32 | eqtri 2765 |
. . . . 5
⊢ (3
· 2) = ;06 |
| 34 | 1, 8, 20, 25, 23, 26, 31, 33 | decmul2c 12799 |
. . . 4
⊢ (3
· ;12) = ;36 |
| 35 | 1, 23, 24, 34 | decsuc 12764 |
. . 3
⊢ ((3
· ;12) + 1) = ;37 |
| 36 | | 1lt3 12439 |
. . 3
⊢ 1 <
3 |
| 37 | 14, 21, 22, 35, 36 | ndvdsi 16449 |
. 2
⊢ ¬ 3
∥ ;37 |
| 38 | | 2nn 12339 |
. . 3
⊢ 2 ∈
ℕ |
| 39 | | 2lt5 12445 |
. . 3
⊢ 2 <
5 |
| 40 | | 5p2e7 12422 |
. . 3
⊢ (5 + 2) =
7 |
| 41 | 1, 38, 39, 40 | dec5dvds2 17103 |
. 2
⊢ ¬ 5
∥ ;37 |
| 42 | | 5nn0 12546 |
. . 3
⊢ 5 ∈
ℕ0 |
| 43 | | 7t5e35 12845 |
. . . 4
⊢ (7
· 5) = ;35 |
| 44 | 1, 42, 20, 43, 40 | decaddi 12793 |
. . 3
⊢ ((7
· 5) + 2) = ;37 |
| 45 | | 2lt7 12456 |
. . 3
⊢ 2 <
7 |
| 46 | 2, 42, 38, 44, 45 | ndvdsi 16449 |
. 2
⊢ ¬ 7
∥ ;37 |
| 47 | 8, 22 | decnncl 12753 |
. . 3
⊢ ;11 ∈ ℕ |
| 48 | | 4nn 12349 |
. . 3
⊢ 4 ∈
ℕ |
| 49 | | eqid 2737 |
. . . 4
⊢ ;11 = ;11 |
| 50 | 27 | mullidi 11266 |
. . . 4
⊢ (1
· 3) = 3 |
| 51 | 50 | oveq1i 7441 |
. . . . 5
⊢ ((1
· 3) + 4) = (3 + 4) |
| 52 | 48 | nncni 12276 |
. . . . . 6
⊢ 4 ∈
ℂ |
| 53 | | 4p3e7 12420 |
. . . . . 6
⊢ (4 + 3) =
7 |
| 54 | 52, 27, 53 | addcomli 11453 |
. . . . 5
⊢ (3 + 4) =
7 |
| 55 | 51, 54 | eqtri 2765 |
. . . 4
⊢ ((1
· 3) + 4) = 7 |
| 56 | 8, 8, 5, 49, 1, 50, 55 | decrmanc 12790 |
. . 3
⊢ ((;11 · 3) + 4) = ;37 |
| 57 | | 4lt10 12869 |
. . . 4
⊢ 4 <
;10 |
| 58 | 22, 8, 5, 57 | declti 12771 |
. . 3
⊢ 4 <
;11 |
| 59 | 47, 1, 48, 56, 58 | ndvdsi 16449 |
. 2
⊢ ¬
;11 ∥ ;37 |
| 60 | 8, 14 | decnncl 12753 |
. . 3
⊢ ;13 ∈ ℕ |
| 61 | | eqid 2737 |
. . . . 5
⊢ ;13 = ;13 |
| 62 | | 2cn 12341 |
. . . . . 6
⊢ 2 ∈
ℂ |
| 63 | 62 | mullidi 11266 |
. . . . 5
⊢ (1
· 2) = 2 |
| 64 | 20, 8, 1, 61, 63, 17 | decmul1 12797 |
. . . 4
⊢ (;13 · 2) = ;26 |
| 65 | | 2p1e3 12408 |
. . . 4
⊢ (2 + 1) =
3 |
| 66 | 20, 23, 8, 8, 64, 49, 65, 24 | decadd 12787 |
. . 3
⊢ ((;13 · 2) + ;11) = ;37 |
| 67 | 8, 8, 14, 36 | declt 12761 |
. . 3
⊢ ;11 < ;13 |
| 68 | 60, 20, 47, 66, 67 | ndvdsi 16449 |
. 2
⊢ ¬
;13 ∥ ;37 |
| 69 | 8, 2 | decnncl 12753 |
. . 3
⊢ ;17 ∈ ℕ |
| 70 | | eqid 2737 |
. . . 4
⊢ ;17 = ;17 |
| 71 | 1 | dec0h 12755 |
. . . 4
⊢ 3 = ;03 |
| 72 | | 0p1e1 12388 |
. . . . . 6
⊢ (0 + 1) =
1 |
| 73 | 63, 72 | oveq12i 7443 |
. . . . 5
⊢ ((1
· 2) + (0 + 1)) = (2 + 1) |
| 74 | 73, 65 | eqtri 2765 |
. . . 4
⊢ ((1
· 2) + (0 + 1)) = 3 |
| 75 | | 7t2e14 12842 |
. . . . 5
⊢ (7
· 2) = ;14 |
| 76 | 8, 5, 1, 75, 53 | decaddi 12793 |
. . . 4
⊢ ((7
· 2) + 3) = ;17 |
| 77 | 8, 7, 26, 1, 70, 71, 20, 7, 8, 74, 76 | decmac 12785 |
. . 3
⊢ ((;17 · 2) + 3) = ;37 |
| 78 | 22, 7, 1, 11 | declti 12771 |
. . 3
⊢ 3 <
;17 |
| 79 | 69, 20, 14, 77, 78 | ndvdsi 16449 |
. 2
⊢ ¬
;17 ∥ ;37 |
| 80 | | 9nn 12364 |
. . . 4
⊢ 9 ∈
ℕ |
| 81 | 8, 80 | decnncl 12753 |
. . 3
⊢ ;19 ∈ ℕ |
| 82 | 8, 10 | decnncl 12753 |
. . 3
⊢ ;18 ∈ ℕ |
| 83 | | 9nn0 12550 |
. . . 4
⊢ 9 ∈
ℕ0 |
| 84 | 81 | nncni 12276 |
. . . . 5
⊢ ;19 ∈ ℂ |
| 85 | 84 | mulridi 11265 |
. . . 4
⊢ (;19 · 1) = ;19 |
| 86 | | eqid 2737 |
. . . 4
⊢ ;18 = ;18 |
| 87 | | 1p1e2 12391 |
. . . . . 6
⊢ (1 + 1) =
2 |
| 88 | 87 | oveq1i 7441 |
. . . . 5
⊢ ((1 + 1)
+ 1) = (2 + 1) |
| 89 | 88, 65 | eqtri 2765 |
. . . 4
⊢ ((1 + 1)
+ 1) = 3 |
| 90 | | 9p8e17 12826 |
. . . 4
⊢ (9 + 8) =
;17 |
| 91 | 8, 83, 8, 4, 85, 86, 89, 7, 90 | decaddc 12788 |
. . 3
⊢ ((;19 · 1) + ;18) = ;37 |
| 92 | | 8lt9 12465 |
. . . 4
⊢ 8 <
9 |
| 93 | 8, 4, 80, 92 | declt 12761 |
. . 3
⊢ ;18 < ;19 |
| 94 | 81, 8, 82, 91, 93 | ndvdsi 16449 |
. 2
⊢ ¬
;19 ∥ ;37 |
| 95 | 20, 14 | decnncl 12753 |
. . 3
⊢ ;23 ∈ ℕ |
| 96 | 8, 48 | decnncl 12753 |
. . 3
⊢ ;14 ∈ ℕ |
| 97 | 95 | nncni 12276 |
. . . . 5
⊢ ;23 ∈ ℂ |
| 98 | 97 | mulridi 11265 |
. . . 4
⊢ (;23 · 1) = ;23 |
| 99 | | eqid 2737 |
. . . 4
⊢ ;14 = ;14 |
| 100 | 20, 1, 8, 5, 98, 99, 65, 54 | decadd 12787 |
. . 3
⊢ ((;23 · 1) + ;14) = ;37 |
| 101 | | 1lt2 12437 |
. . . 4
⊢ 1 <
2 |
| 102 | 8, 20, 5, 1, 57, 101 | decltc 12762 |
. . 3
⊢ ;14 < ;23 |
| 103 | 95, 8, 96, 100, 102 | ndvdsi 16449 |
. 2
⊢ ¬
;23 ∥ ;37 |
| 104 | 3, 13, 16, 19, 37, 41, 46, 59, 68, 79, 94, 103 | prmlem2 17157 |
1
⊢ ;37 ∈ ℙ |