Proof of Theorem 139prm
| Step | Hyp | Ref
| Expression |
| 1 | | 1nn0 12542 |
. . . 4
⊢ 1 ∈
ℕ0 |
| 2 | | 3nn0 12544 |
. . . 4
⊢ 3 ∈
ℕ0 |
| 3 | 1, 2 | deccl 12748 |
. . 3
⊢ ;13 ∈
ℕ0 |
| 4 | | 9nn 12364 |
. . 3
⊢ 9 ∈
ℕ |
| 5 | 3, 4 | decnncl 12753 |
. 2
⊢ ;;139 ∈ ℕ |
| 6 | | 8nn0 12549 |
. . 3
⊢ 8 ∈
ℕ0 |
| 7 | | 4nn0 12545 |
. . 3
⊢ 4 ∈
ℕ0 |
| 8 | | 9nn0 12550 |
. . 3
⊢ 9 ∈
ℕ0 |
| 9 | | 1lt8 12464 |
. . 3
⊢ 1 <
8 |
| 10 | | 3lt10 12870 |
. . 3
⊢ 3 <
;10 |
| 11 | | 9lt10 12864 |
. . 3
⊢ 9 <
;10 |
| 12 | 1, 6, 2, 7, 8, 1, 9, 10, 11 | 3decltc 12766 |
. 2
⊢ ;;139 < ;;841 |
| 13 | | 3nn 12345 |
. . . 4
⊢ 3 ∈
ℕ |
| 14 | 1, 13 | decnncl 12753 |
. . 3
⊢ ;13 ∈ ℕ |
| 15 | | 1lt10 12872 |
. . 3
⊢ 1 <
;10 |
| 16 | 14, 8, 1, 15 | declti 12771 |
. 2
⊢ 1 <
;;139 |
| 17 | | 4t2e8 12434 |
. . 3
⊢ (4
· 2) = 8 |
| 18 | | df-9 12336 |
. . 3
⊢ 9 = (8 +
1) |
| 19 | 3, 7, 17, 18 | dec2dvds 17101 |
. 2
⊢ ¬ 2
∥ ;;139 |
| 20 | | 6nn0 12547 |
. . . 4
⊢ 6 ∈
ℕ0 |
| 21 | 7, 20 | deccl 12748 |
. . 3
⊢ ;46 ∈
ℕ0 |
| 22 | | 1nn 12277 |
. . 3
⊢ 1 ∈
ℕ |
| 23 | | 0nn0 12541 |
. . . 4
⊢ 0 ∈
ℕ0 |
| 24 | | eqid 2737 |
. . . 4
⊢ ;46 = ;46 |
| 25 | 1 | dec0h 12755 |
. . . 4
⊢ 1 = ;01 |
| 26 | | ax-1cn 11213 |
. . . . . . 7
⊢ 1 ∈
ℂ |
| 27 | 26 | addlidi 11449 |
. . . . . 6
⊢ (0 + 1) =
1 |
| 28 | 27 | oveq2i 7442 |
. . . . 5
⊢ ((3
· 4) + (0 + 1)) = ((3 · 4) + 1) |
| 29 | | 2nn0 12543 |
. . . . . 6
⊢ 2 ∈
ℕ0 |
| 30 | | 2p1e3 12408 |
. . . . . 6
⊢ (2 + 1) =
3 |
| 31 | 7 | nn0cni 12538 |
. . . . . . 7
⊢ 4 ∈
ℂ |
| 32 | | 3cn 12347 |
. . . . . . 7
⊢ 3 ∈
ℂ |
| 33 | | 4t3e12 12831 |
. . . . . . 7
⊢ (4
· 3) = ;12 |
| 34 | 31, 32, 33 | mulcomli 11270 |
. . . . . 6
⊢ (3
· 4) = ;12 |
| 35 | 1, 29, 30, 34 | decsuc 12764 |
. . . . 5
⊢ ((3
· 4) + 1) = ;13 |
| 36 | 28, 35 | eqtri 2765 |
. . . 4
⊢ ((3
· 4) + (0 + 1)) = ;13 |
| 37 | | 8p1e9 12416 |
. . . . 5
⊢ (8 + 1) =
9 |
| 38 | 20 | nn0cni 12538 |
. . . . . 6
⊢ 6 ∈
ℂ |
| 39 | | 6t3e18 12838 |
. . . . . 6
⊢ (6
· 3) = ;18 |
| 40 | 38, 32, 39 | mulcomli 11270 |
. . . . 5
⊢ (3
· 6) = ;18 |
| 41 | 1, 6, 37, 40 | decsuc 12764 |
. . . 4
⊢ ((3
· 6) + 1) = ;19 |
| 42 | 7, 20, 23, 1, 24, 25, 2, 8, 1,
36, 41 | decma2c 12786 |
. . 3
⊢ ((3
· ;46) + 1) = ;;139 |
| 43 | | 1lt3 12439 |
. . 3
⊢ 1 <
3 |
| 44 | 13, 21, 22, 42, 43 | ndvdsi 16449 |
. 2
⊢ ¬ 3
∥ ;;139 |
| 45 | | 4nn 12349 |
. . 3
⊢ 4 ∈
ℕ |
| 46 | | 4lt5 12443 |
. . 3
⊢ 4 <
5 |
| 47 | | 5p4e9 12424 |
. . 3
⊢ (5 + 4) =
9 |
| 48 | 3, 45, 46, 47 | dec5dvds2 17103 |
. 2
⊢ ¬ 5
∥ ;;139 |
| 49 | | 7nn 12358 |
. . 3
⊢ 7 ∈
ℕ |
| 50 | 1, 8 | deccl 12748 |
. . 3
⊢ ;19 ∈
ℕ0 |
| 51 | | 6nn 12355 |
. . 3
⊢ 6 ∈
ℕ |
| 52 | | eqid 2737 |
. . . 4
⊢ ;19 = ;19 |
| 53 | 20 | dec0h 12755 |
. . . 4
⊢ 6 = ;06 |
| 54 | | 7nn0 12548 |
. . . 4
⊢ 7 ∈
ℕ0 |
| 55 | | 7cn 12360 |
. . . . . . 7
⊢ 7 ∈
ℂ |
| 56 | 55 | mulridi 11265 |
. . . . . 6
⊢ (7
· 1) = 7 |
| 57 | 38 | addlidi 11449 |
. . . . . 6
⊢ (0 + 6) =
6 |
| 58 | 56, 57 | oveq12i 7443 |
. . . . 5
⊢ ((7
· 1) + (0 + 6)) = (7 + 6) |
| 59 | | 7p6e13 12811 |
. . . . 5
⊢ (7 + 6) =
;13 |
| 60 | 58, 59 | eqtri 2765 |
. . . 4
⊢ ((7
· 1) + (0 + 6)) = ;13 |
| 61 | | 9cn 12366 |
. . . . . 6
⊢ 9 ∈
ℂ |
| 62 | | 9t7e63 12860 |
. . . . . 6
⊢ (9
· 7) = ;63 |
| 63 | 61, 55, 62 | mulcomli 11270 |
. . . . 5
⊢ (7
· 9) = ;63 |
| 64 | | 6p3e9 12426 |
. . . . . 6
⊢ (6 + 3) =
9 |
| 65 | 38, 32, 64 | addcomli 11453 |
. . . . 5
⊢ (3 + 6) =
9 |
| 66 | 20, 2, 20, 63, 65 | decaddi 12793 |
. . . 4
⊢ ((7
· 9) + 6) = ;69 |
| 67 | 1, 8, 23, 20, 52, 53, 54, 8, 20, 60, 66 | decma2c 12786 |
. . 3
⊢ ((7
· ;19) + 6) = ;;139 |
| 68 | | 6lt7 12452 |
. . 3
⊢ 6 <
7 |
| 69 | 49, 50, 51, 67, 68 | ndvdsi 16449 |
. 2
⊢ ¬ 7
∥ ;;139 |
| 70 | 1, 22 | decnncl 12753 |
. . 3
⊢ ;11 ∈ ℕ |
| 71 | 1, 29 | deccl 12748 |
. . 3
⊢ ;12 ∈
ℕ0 |
| 72 | | eqid 2737 |
. . . 4
⊢ ;12 = ;12 |
| 73 | 54 | dec0h 12755 |
. . . 4
⊢ 7 = ;07 |
| 74 | 1, 1 | deccl 12748 |
. . . 4
⊢ ;11 ∈
ℕ0 |
| 75 | | 2cn 12341 |
. . . . . . 7
⊢ 2 ∈
ℂ |
| 76 | 75 | addlidi 11449 |
. . . . . 6
⊢ (0 + 2) =
2 |
| 77 | 76 | oveq2i 7442 |
. . . . 5
⊢ ((;11 · 1) + (0 + 2)) = ((;11 · 1) + 2) |
| 78 | 70 | nncni 12276 |
. . . . . . 7
⊢ ;11 ∈ ℂ |
| 79 | 78 | mulridi 11265 |
. . . . . 6
⊢ (;11 · 1) = ;11 |
| 80 | | 1p2e3 12409 |
. . . . . 6
⊢ (1 + 2) =
3 |
| 81 | 1, 1, 29, 79, 80 | decaddi 12793 |
. . . . 5
⊢ ((;11 · 1) + 2) = ;13 |
| 82 | 77, 81 | eqtri 2765 |
. . . 4
⊢ ((;11 · 1) + (0 + 2)) = ;13 |
| 83 | | eqid 2737 |
. . . . 5
⊢ ;11 = ;11 |
| 84 | 75 | mullidi 11266 |
. . . . . . 7
⊢ (1
· 2) = 2 |
| 85 | | 00id 11436 |
. . . . . . 7
⊢ (0 + 0) =
0 |
| 86 | 84, 85 | oveq12i 7443 |
. . . . . 6
⊢ ((1
· 2) + (0 + 0)) = (2 + 0) |
| 87 | 75 | addridi 11448 |
. . . . . 6
⊢ (2 + 0) =
2 |
| 88 | 86, 87 | eqtri 2765 |
. . . . 5
⊢ ((1
· 2) + (0 + 0)) = 2 |
| 89 | 84 | oveq1i 7441 |
. . . . . 6
⊢ ((1
· 2) + 7) = (2 + 7) |
| 90 | | 7p2e9 12427 |
. . . . . . 7
⊢ (7 + 2) =
9 |
| 91 | 55, 75, 90 | addcomli 11453 |
. . . . . 6
⊢ (2 + 7) =
9 |
| 92 | 8 | dec0h 12755 |
. . . . . 6
⊢ 9 = ;09 |
| 93 | 89, 91, 92 | 3eqtri 2769 |
. . . . 5
⊢ ((1
· 2) + 7) = ;09 |
| 94 | 1, 1, 23, 54, 83, 73, 29, 8, 23, 88, 93 | decmac 12785 |
. . . 4
⊢ ((;11 · 2) + 7) = ;29 |
| 95 | 1, 29, 23, 54, 72, 73, 74, 8, 29, 82, 94 | decma2c 12786 |
. . 3
⊢ ((;11 · ;12) + 7) = ;;139 |
| 96 | | 7lt10 12866 |
. . . 4
⊢ 7 <
;10 |
| 97 | 22, 1, 54, 96 | declti 12771 |
. . 3
⊢ 7 <
;11 |
| 98 | 70, 71, 49, 95, 97 | ndvdsi 16449 |
. 2
⊢ ¬
;11 ∥ ;;139 |
| 99 | | 10nn0 12751 |
. . 3
⊢ ;10 ∈
ℕ0 |
| 100 | | eqid 2737 |
. . . 4
⊢ ;10 = ;10 |
| 101 | | eqid 2737 |
. . . . 5
⊢ ;13 = ;13 |
| 102 | 23 | dec0h 12755 |
. . . . . 6
⊢ 0 = ;00 |
| 103 | 85, 102 | eqtri 2765 |
. . . . 5
⊢ (0 + 0) =
;00 |
| 104 | 26 | mulridi 11265 |
. . . . . . 7
⊢ (1
· 1) = 1 |
| 105 | 104, 85 | oveq12i 7443 |
. . . . . 6
⊢ ((1
· 1) + (0 + 0)) = (1 + 0) |
| 106 | 26 | addridi 11448 |
. . . . . 6
⊢ (1 + 0) =
1 |
| 107 | 105, 106 | eqtri 2765 |
. . . . 5
⊢ ((1
· 1) + (0 + 0)) = 1 |
| 108 | 32 | mulridi 11265 |
. . . . . . 7
⊢ (3
· 1) = 3 |
| 109 | 108 | oveq1i 7441 |
. . . . . 6
⊢ ((3
· 1) + 0) = (3 + 0) |
| 110 | 32 | addridi 11448 |
. . . . . 6
⊢ (3 + 0) =
3 |
| 111 | 2 | dec0h 12755 |
. . . . . 6
⊢ 3 = ;03 |
| 112 | 109, 110,
111 | 3eqtri 2769 |
. . . . 5
⊢ ((3
· 1) + 0) = ;03 |
| 113 | 1, 2, 23, 23, 101, 103, 1, 2, 23, 107, 112 | decmac 12785 |
. . . 4
⊢ ((;13 · 1) + (0 + 0)) = ;13 |
| 114 | 3 | nn0cni 12538 |
. . . . . . 7
⊢ ;13 ∈ ℂ |
| 115 | 114 | mul01i 11451 |
. . . . . 6
⊢ (;13 · 0) = 0 |
| 116 | 115 | oveq1i 7441 |
. . . . 5
⊢ ((;13 · 0) + 9) = (0 +
9) |
| 117 | 61 | addlidi 11449 |
. . . . 5
⊢ (0 + 9) =
9 |
| 118 | 116, 117,
92 | 3eqtri 2769 |
. . . 4
⊢ ((;13 · 0) + 9) = ;09 |
| 119 | 1, 23, 23, 8, 100, 92, 3, 8, 23, 113, 118 | decma2c 12786 |
. . 3
⊢ ((;13 · ;10) + 9) = ;;139 |
| 120 | 22, 2, 8, 11 | declti 12771 |
. . 3
⊢ 9 <
;13 |
| 121 | 14, 99, 4, 119, 120 | ndvdsi 16449 |
. 2
⊢ ¬
;13 ∥ ;;139 |
| 122 | 1, 49 | decnncl 12753 |
. . 3
⊢ ;17 ∈ ℕ |
| 123 | | eqid 2737 |
. . . 4
⊢ ;17 = ;17 |
| 124 | | 5nn0 12546 |
. . . 4
⊢ 5 ∈
ℕ0 |
| 125 | | 8cn 12363 |
. . . . . . 7
⊢ 8 ∈
ℂ |
| 126 | 125 | mullidi 11266 |
. . . . . 6
⊢ (1
· 8) = 8 |
| 127 | | 5cn 12354 |
. . . . . . 7
⊢ 5 ∈
ℂ |
| 128 | 127 | addlidi 11449 |
. . . . . 6
⊢ (0 + 5) =
5 |
| 129 | 126, 128 | oveq12i 7443 |
. . . . 5
⊢ ((1
· 8) + (0 + 5)) = (8 + 5) |
| 130 | | 8p5e13 12816 |
. . . . 5
⊢ (8 + 5) =
;13 |
| 131 | 129, 130 | eqtri 2765 |
. . . 4
⊢ ((1
· 8) + (0 + 5)) = ;13 |
| 132 | | 8t7e56 12853 |
. . . . . 6
⊢ (8
· 7) = ;56 |
| 133 | 125, 55, 132 | mulcomli 11270 |
. . . . 5
⊢ (7
· 8) = ;56 |
| 134 | 124, 20, 2, 133, 64 | decaddi 12793 |
. . . 4
⊢ ((7
· 8) + 3) = ;59 |
| 135 | 1, 54, 23, 2, 123, 111, 6, 8, 124, 131, 134 | decmac 12785 |
. . 3
⊢ ((;17 · 8) + 3) = ;;139 |
| 136 | 22, 54, 2, 10 | declti 12771 |
. . 3
⊢ 3 <
;17 |
| 137 | 122, 6, 13, 135, 136 | ndvdsi 16449 |
. 2
⊢ ¬
;17 ∥ ;;139 |
| 138 | 1, 4 | decnncl 12753 |
. . 3
⊢ ;19 ∈ ℕ |
| 139 | 55 | mullidi 11266 |
. . . . . 6
⊢ (1
· 7) = 7 |
| 140 | 139, 57 | oveq12i 7443 |
. . . . 5
⊢ ((1
· 7) + (0 + 6)) = (7 + 6) |
| 141 | 140, 59 | eqtri 2765 |
. . . 4
⊢ ((1
· 7) + (0 + 6)) = ;13 |
| 142 | 20, 2, 20, 62, 65 | decaddi 12793 |
. . . 4
⊢ ((9
· 7) + 6) = ;69 |
| 143 | 1, 8, 23, 20, 52, 53, 54, 8, 20, 141, 142 | decmac 12785 |
. . 3
⊢ ((;19 · 7) + 6) = ;;139 |
| 144 | | 6lt10 12867 |
. . . 4
⊢ 6 <
;10 |
| 145 | 22, 8, 20, 144 | declti 12771 |
. . 3
⊢ 6 <
;19 |
| 146 | 138, 54, 51, 143, 145 | ndvdsi 16449 |
. 2
⊢ ¬
;19 ∥ ;;139 |
| 147 | 29, 13 | decnncl 12753 |
. . 3
⊢ ;23 ∈ ℕ |
| 148 | | eqid 2737 |
. . . 4
⊢ ;23 = ;23 |
| 149 | | 6t2e12 12837 |
. . . . . 6
⊢ (6
· 2) = ;12 |
| 150 | 38, 75, 149 | mulcomli 11270 |
. . . . 5
⊢ (2
· 6) = ;12 |
| 151 | 1, 29, 30, 150 | decsuc 12764 |
. . . 4
⊢ ((2
· 6) + 1) = ;13 |
| 152 | 29, 2, 1, 148, 20, 8, 1, 151, 41 | decrmac 12791 |
. . 3
⊢ ((;23 · 6) + 1) = ;;139 |
| 153 | | 2nn 12339 |
. . . 4
⊢ 2 ∈
ℕ |
| 154 | 153, 2, 1, 15 | declti 12771 |
. . 3
⊢ 1 <
;23 |
| 155 | 147, 20, 22, 152, 154 | ndvdsi 16449 |
. 2
⊢ ¬
;23 ∥ ;;139 |
| 156 | 5, 12, 16, 19, 44, 48, 69, 98, 121, 137, 146, 155 | prmlem2 17157 |
1
⊢ ;;139 ∈ ℙ |