Proof of Theorem 139prmALT
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1nn0 12544 | . . . 4
⊢ 1 ∈
ℕ0 | 
| 2 |  | 3nn0 12546 | . . . 4
⊢ 3 ∈
ℕ0 | 
| 3 | 1, 2 | deccl 12750 | . . 3
⊢ ;13 ∈
ℕ0 | 
| 4 |  | 9nn 12365 | . . 3
⊢ 9 ∈
ℕ | 
| 5 | 3, 4 | decnncl 12755 | . 2
⊢ ;;139 ∈ ℕ | 
| 6 |  | 8nn0 12551 | . . 3
⊢ 8 ∈
ℕ0 | 
| 7 |  | 4nn0 12547 | . . 3
⊢ 4 ∈
ℕ0 | 
| 8 |  | 9nn0 12552 | . . 3
⊢ 9 ∈
ℕ0 | 
| 9 |  | 1lt8 12465 | . . 3
⊢ 1 <
8 | 
| 10 |  | 3lt10 12872 | . . 3
⊢ 3 <
;10 | 
| 11 |  | 9lt10 12866 | . . 3
⊢ 9 <
;10 | 
| 12 | 1, 6, 2, 7, 8, 1, 9, 10, 11 | 3decltc 12768 | . 2
⊢ ;;139 < ;;841 | 
| 13 |  | 3nn 12346 | . . . 4
⊢ 3 ∈
ℕ | 
| 14 | 1, 13 | decnncl 12755 | . . 3
⊢ ;13 ∈ ℕ | 
| 15 |  | 1lt10 12874 | . . 3
⊢ 1 <
;10 | 
| 16 | 14, 8, 1, 15 | declti 12773 | . 2
⊢ 1 <
;;139 | 
| 17 |  | 4t2e8 12435 | . . 3
⊢ (4
· 2) = 8 | 
| 18 |  | df-9 12337 | . . 3
⊢ 9 = (8 +
1) | 
| 19 | 3, 7, 17, 18 | dec2dvds 17102 | . 2
⊢  ¬ 2
∥ ;;139 | 
| 20 |  | 3ndvds4 47587 | . . . 4
⊢  ¬ 3
∥ 4 | 
| 21 | 1, 2 | 3dvdsdec 16370 | . . . . 5
⊢ (3
∥ ;13 ↔ 3 ∥ (1 +
3)) | 
| 22 |  | 3cn 12348 | . . . . . . 7
⊢ 3 ∈
ℂ | 
| 23 |  | ax-1cn 11214 | . . . . . . 7
⊢ 1 ∈
ℂ | 
| 24 |  | 3p1e4 12412 | . . . . . . 7
⊢ (3 + 1) =
4 | 
| 25 | 22, 23, 24 | addcomli 11454 | . . . . . 6
⊢ (1 + 3) =
4 | 
| 26 | 25 | breq2i 5150 | . . . . 5
⊢ (3
∥ (1 + 3) ↔ 3 ∥ 4) | 
| 27 | 21, 26 | bitri 275 | . . . 4
⊢ (3
∥ ;13 ↔ 3 ∥
4) | 
| 28 | 20, 27 | mtbir 323 | . . 3
⊢  ¬ 3
∥ ;13 | 
| 29 | 1, 2, 8 | 3dvds2dec 16371 | . . . 4
⊢ (3
∥ ;;139 ↔ 3 ∥ ((1 + 3) + 9)) | 
| 30 | 25 | oveq1i 7442 | . . . . . 6
⊢ ((1 + 3)
+ 9) = (4 + 9) | 
| 31 |  | 9cn 12367 | . . . . . . 7
⊢ 9 ∈
ℂ | 
| 32 |  | 4cn 12352 | . . . . . . 7
⊢ 4 ∈
ℂ | 
| 33 |  | 9p4e13 12824 | . . . . . . 7
⊢ (9 + 4) =
;13 | 
| 34 | 31, 32, 33 | addcomli 11454 | . . . . . 6
⊢ (4 + 9) =
;13 | 
| 35 | 30, 34 | eqtri 2764 | . . . . 5
⊢ ((1 + 3)
+ 9) = ;13 | 
| 36 | 35 | breq2i 5150 | . . . 4
⊢ (3
∥ ((1 + 3) + 9) ↔ 3 ∥ ;13) | 
| 37 | 29, 36 | bitri 275 | . . 3
⊢ (3
∥ ;;139 ↔ 3 ∥ ;13) | 
| 38 | 28, 37 | mtbir 323 | . 2
⊢  ¬ 3
∥ ;;139 | 
| 39 |  | 4nn 12350 | . . 3
⊢ 4 ∈
ℕ | 
| 40 |  | 4lt5 12444 | . . 3
⊢ 4 <
5 | 
| 41 |  | 5p4e9 12425 | . . 3
⊢ (5 + 4) =
9 | 
| 42 | 3, 39, 40, 41 | dec5dvds2 17104 | . 2
⊢  ¬ 5
∥ ;;139 | 
| 43 |  | 7nn 12359 | . . 3
⊢ 7 ∈
ℕ | 
| 44 | 1, 8 | deccl 12750 | . . 3
⊢ ;19 ∈
ℕ0 | 
| 45 |  | 6nn 12356 | . . 3
⊢ 6 ∈
ℕ | 
| 46 |  | 0nn0 12543 | . . . 4
⊢ 0 ∈
ℕ0 | 
| 47 |  | 6nn0 12549 | . . . 4
⊢ 6 ∈
ℕ0 | 
| 48 |  | eqid 2736 | . . . 4
⊢ ;19 = ;19 | 
| 49 | 47 | dec0h 12757 | . . . 4
⊢ 6 = ;06 | 
| 50 |  | 7nn0 12550 | . . . 4
⊢ 7 ∈
ℕ0 | 
| 51 |  | 7cn 12361 | . . . . . . 7
⊢ 7 ∈
ℂ | 
| 52 | 51 | mulridi 11266 | . . . . . 6
⊢ (7
· 1) = 7 | 
| 53 |  | 6cn 12358 | . . . . . . 7
⊢ 6 ∈
ℂ | 
| 54 | 53 | addlidi 11450 | . . . . . 6
⊢ (0 + 6) =
6 | 
| 55 | 52, 54 | oveq12i 7444 | . . . . 5
⊢ ((7
· 1) + (0 + 6)) = (7 + 6) | 
| 56 |  | 7p6e13 12813 | . . . . 5
⊢ (7 + 6) =
;13 | 
| 57 | 55, 56 | eqtri 2764 | . . . 4
⊢ ((7
· 1) + (0 + 6)) = ;13 | 
| 58 |  | 9t7e63 12862 | . . . . . 6
⊢ (9
· 7) = ;63 | 
| 59 | 31, 51, 58 | mulcomli 11271 | . . . . 5
⊢ (7
· 9) = ;63 | 
| 60 |  | 6p3e9 12427 | . . . . . 6
⊢ (6 + 3) =
9 | 
| 61 | 53, 22, 60 | addcomli 11454 | . . . . 5
⊢ (3 + 6) =
9 | 
| 62 | 47, 2, 47, 59, 61 | decaddi 12795 | . . . 4
⊢ ((7
· 9) + 6) = ;69 | 
| 63 | 1, 8, 46, 47, 48, 49, 50, 8, 47, 57, 62 | decma2c 12788 | . . 3
⊢ ((7
· ;19) + 6) = ;;139 | 
| 64 |  | 6lt7 12453 | . . 3
⊢ 6 <
7 | 
| 65 | 43, 44, 45, 63, 64 | ndvdsi 16450 | . 2
⊢  ¬ 7
∥ ;;139 | 
| 66 |  | 1nn 12278 | . . . 4
⊢ 1 ∈
ℕ | 
| 67 | 1, 66 | decnncl 12755 | . . 3
⊢ ;11 ∈ ℕ | 
| 68 |  | 2nn0 12545 | . . . 4
⊢ 2 ∈
ℕ0 | 
| 69 | 1, 68 | deccl 12750 | . . 3
⊢ ;12 ∈
ℕ0 | 
| 70 |  | eqid 2736 | . . . 4
⊢ ;12 = ;12 | 
| 71 | 50 | dec0h 12757 | . . . 4
⊢ 7 = ;07 | 
| 72 | 1, 1 | deccl 12750 | . . . 4
⊢ ;11 ∈
ℕ0 | 
| 73 |  | 2cn 12342 | . . . . . . 7
⊢ 2 ∈
ℂ | 
| 74 | 73 | addlidi 11450 | . . . . . 6
⊢ (0 + 2) =
2 | 
| 75 | 74 | oveq2i 7443 | . . . . 5
⊢ ((;11 · 1) + (0 + 2)) = ((;11 · 1) + 2) | 
| 76 | 67 | nncni 12277 | . . . . . . 7
⊢ ;11 ∈ ℂ | 
| 77 | 76 | mulridi 11266 | . . . . . 6
⊢ (;11 · 1) = ;11 | 
| 78 |  | 1p2e3 12410 | . . . . . 6
⊢ (1 + 2) =
3 | 
| 79 | 1, 1, 68, 77, 78 | decaddi 12795 | . . . . 5
⊢ ((;11 · 1) + 2) = ;13 | 
| 80 | 75, 79 | eqtri 2764 | . . . 4
⊢ ((;11 · 1) + (0 + 2)) = ;13 | 
| 81 |  | eqid 2736 | . . . . 5
⊢ ;11 = ;11 | 
| 82 | 73 | mullidi 11267 | . . . . . . 7
⊢ (1
· 2) = 2 | 
| 83 |  | 00id 11437 | . . . . . . 7
⊢ (0 + 0) =
0 | 
| 84 | 82, 83 | oveq12i 7444 | . . . . . 6
⊢ ((1
· 2) + (0 + 0)) = (2 + 0) | 
| 85 | 73 | addridi 11449 | . . . . . 6
⊢ (2 + 0) =
2 | 
| 86 | 84, 85 | eqtri 2764 | . . . . 5
⊢ ((1
· 2) + (0 + 0)) = 2 | 
| 87 | 82 | oveq1i 7442 | . . . . . 6
⊢ ((1
· 2) + 7) = (2 + 7) | 
| 88 |  | 7p2e9 12428 | . . . . . . 7
⊢ (7 + 2) =
9 | 
| 89 | 51, 73, 88 | addcomli 11454 | . . . . . 6
⊢ (2 + 7) =
9 | 
| 90 | 8 | dec0h 12757 | . . . . . 6
⊢ 9 = ;09 | 
| 91 | 87, 89, 90 | 3eqtri 2768 | . . . . 5
⊢ ((1
· 2) + 7) = ;09 | 
| 92 | 1, 1, 46, 50, 81, 71, 68, 8, 46, 86, 91 | decmac 12787 | . . . 4
⊢ ((;11 · 2) + 7) = ;29 | 
| 93 | 1, 68, 46, 50, 70, 71, 72, 8, 68, 80, 92 | decma2c 12788 | . . 3
⊢ ((;11 · ;12) + 7) = ;;139 | 
| 94 |  | 7lt10 12868 | . . . 4
⊢ 7 <
;10 | 
| 95 | 66, 1, 50, 94 | declti 12773 | . . 3
⊢ 7 <
;11 | 
| 96 | 67, 69, 43, 93, 95 | ndvdsi 16450 | . 2
⊢  ¬
;11 ∥ ;;139 | 
| 97 | 1, 46 | deccl 12750 | . . 3
⊢ ;10 ∈
ℕ0 | 
| 98 |  | eqid 2736 | . . . 4
⊢ ;10 = ;10 | 
| 99 | 3 | nn0cni 12540 | . . . . . . 7
⊢ ;13 ∈ ℂ | 
| 100 | 99 | mulridi 11266 | . . . . . 6
⊢ (;13 · 1) = ;13 | 
| 101 | 100, 83 | oveq12i 7444 | . . . . 5
⊢ ((;13 · 1) + (0 + 0)) = (;13 + 0) | 
| 102 | 99 | addridi 11449 | . . . . 5
⊢ (;13 + 0) = ;13 | 
| 103 | 101, 102 | eqtri 2764 | . . . 4
⊢ ((;13 · 1) + (0 + 0)) = ;13 | 
| 104 | 99 | mul01i 11452 | . . . . . 6
⊢ (;13 · 0) = 0 | 
| 105 | 104 | oveq1i 7442 | . . . . 5
⊢ ((;13 · 0) + 9) = (0 +
9) | 
| 106 | 31 | addlidi 11450 | . . . . 5
⊢ (0 + 9) =
9 | 
| 107 | 105, 106,
90 | 3eqtri 2768 | . . . 4
⊢ ((;13 · 0) + 9) = ;09 | 
| 108 | 1, 46, 46, 8, 98, 90, 3, 8, 46, 103, 107 | decma2c 12788 | . . 3
⊢ ((;13 · ;10) + 9) = ;;139 | 
| 109 | 66, 2, 8, 11 | declti 12773 | . . 3
⊢ 9 <
;13 | 
| 110 | 14, 97, 4, 108, 109 | ndvdsi 16450 | . 2
⊢  ¬
;13 ∥ ;;139 | 
| 111 | 1, 43 | decnncl 12755 | . . 3
⊢ ;17 ∈ ℕ | 
| 112 |  | eqid 2736 | . . . 4
⊢ ;17 = ;17 | 
| 113 | 2 | dec0h 12757 | . . . 4
⊢ 3 = ;03 | 
| 114 |  | 5nn0 12548 | . . . 4
⊢ 5 ∈
ℕ0 | 
| 115 |  | 8cn 12364 | . . . . . . 7
⊢ 8 ∈
ℂ | 
| 116 | 115 | mullidi 11267 | . . . . . 6
⊢ (1
· 8) = 8 | 
| 117 |  | 5cn 12355 | . . . . . . 7
⊢ 5 ∈
ℂ | 
| 118 | 117 | addlidi 11450 | . . . . . 6
⊢ (0 + 5) =
5 | 
| 119 | 116, 118 | oveq12i 7444 | . . . . 5
⊢ ((1
· 8) + (0 + 5)) = (8 + 5) | 
| 120 |  | 8p5e13 12818 | . . . . 5
⊢ (8 + 5) =
;13 | 
| 121 | 119, 120 | eqtri 2764 | . . . 4
⊢ ((1
· 8) + (0 + 5)) = ;13 | 
| 122 |  | 8t7e56 12855 | . . . . . 6
⊢ (8
· 7) = ;56 | 
| 123 | 115, 51, 122 | mulcomli 11271 | . . . . 5
⊢ (7
· 8) = ;56 | 
| 124 | 114, 47, 2, 123, 60 | decaddi 12795 | . . . 4
⊢ ((7
· 8) + 3) = ;59 | 
| 125 | 1, 50, 46, 2, 112, 113, 6, 8, 114, 121, 124 | decmac 12787 | . . 3
⊢ ((;17 · 8) + 3) = ;;139 | 
| 126 | 66, 50, 2, 10 | declti 12773 | . . 3
⊢ 3 <
;17 | 
| 127 | 111, 6, 13, 125, 126 | ndvdsi 16450 | . 2
⊢  ¬
;17 ∥ ;;139 | 
| 128 | 1, 4 | decnncl 12755 | . . 3
⊢ ;19 ∈ ℕ | 
| 129 | 51 | mullidi 11267 | . . . . . 6
⊢ (1
· 7) = 7 | 
| 130 | 129, 54 | oveq12i 7444 | . . . . 5
⊢ ((1
· 7) + (0 + 6)) = (7 + 6) | 
| 131 | 130, 56 | eqtri 2764 | . . . 4
⊢ ((1
· 7) + (0 + 6)) = ;13 | 
| 132 | 47, 2, 47, 58, 61 | decaddi 12795 | . . . 4
⊢ ((9
· 7) + 6) = ;69 | 
| 133 | 1, 8, 46, 47, 48, 49, 50, 8, 47, 131, 132 | decmac 12787 | . . 3
⊢ ((;19 · 7) + 6) = ;;139 | 
| 134 |  | 6lt10 12869 | . . . 4
⊢ 6 <
;10 | 
| 135 | 66, 8, 47, 134 | declti 12773 | . . 3
⊢ 6 <
;19 | 
| 136 | 128, 50, 45, 133, 135 | ndvdsi 16450 | . 2
⊢  ¬
;19 ∥ ;;139 | 
| 137 | 68, 13 | decnncl 12755 | . . 3
⊢ ;23 ∈ ℕ | 
| 138 |  | eqid 2736 | . . . 4
⊢ ;23 = ;23 | 
| 139 |  | 2p1e3 12409 | . . . . 5
⊢ (2 + 1) =
3 | 
| 140 |  | 6t2e12 12839 | . . . . . 6
⊢ (6
· 2) = ;12 | 
| 141 | 53, 73, 140 | mulcomli 11271 | . . . . 5
⊢ (2
· 6) = ;12 | 
| 142 | 1, 68, 139, 141 | decsuc 12766 | . . . 4
⊢ ((2
· 6) + 1) = ;13 | 
| 143 |  | 8p1e9 12417 | . . . . 5
⊢ (8 + 1) =
9 | 
| 144 |  | 6t3e18 12840 | . . . . . 6
⊢ (6
· 3) = ;18 | 
| 145 | 53, 22, 144 | mulcomli 11271 | . . . . 5
⊢ (3
· 6) = ;18 | 
| 146 | 1, 6, 143, 145 | decsuc 12766 | . . . 4
⊢ ((3
· 6) + 1) = ;19 | 
| 147 | 68, 2, 1, 138, 47, 8, 1, 142, 146 | decrmac 12793 | . . 3
⊢ ((;23 · 6) + 1) = ;;139 | 
| 148 |  | 2nn 12340 | . . . 4
⊢ 2 ∈
ℕ | 
| 149 | 148, 2, 1, 15 | declti 12773 | . . 3
⊢ 1 <
;23 | 
| 150 | 137, 47, 66, 147, 149 | ndvdsi 16450 | . 2
⊢  ¬
;23 ∥ ;;139 | 
| 151 | 5, 12, 16, 19, 38, 42, 65, 96, 110, 127, 136, 150 | prmlem2 17158 | 1
⊢ ;;139 ∈ ℙ |