Proof of Theorem 1259lem2
| Step | Hyp | Ref
| Expression |
| 1 | | 1259prm.1 |
. . 3
⊢ 𝑁 = ;;;1259 |
| 2 | | 1nn0 12542 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
| 3 | | 2nn0 12543 |
. . . . . 6
⊢ 2 ∈
ℕ0 |
| 4 | 2, 3 | deccl 12748 |
. . . . 5
⊢ ;12 ∈
ℕ0 |
| 5 | | 5nn0 12546 |
. . . . 5
⊢ 5 ∈
ℕ0 |
| 6 | 4, 5 | deccl 12748 |
. . . 4
⊢ ;;125 ∈ ℕ0 |
| 7 | | 9nn 12364 |
. . . 4
⊢ 9 ∈
ℕ |
| 8 | 6, 7 | decnncl 12753 |
. . 3
⊢ ;;;1259
∈ ℕ |
| 9 | 1, 8 | eqeltri 2837 |
. 2
⊢ 𝑁 ∈ ℕ |
| 10 | | 2nn 12339 |
. 2
⊢ 2 ∈
ℕ |
| 11 | | 7nn0 12548 |
. . 3
⊢ 7 ∈
ℕ0 |
| 12 | 2, 11 | deccl 12748 |
. 2
⊢ ;17 ∈
ℕ0 |
| 13 | | 4nn0 12545 |
. . . 4
⊢ 4 ∈
ℕ0 |
| 14 | 2, 13 | deccl 12748 |
. . 3
⊢ ;14 ∈
ℕ0 |
| 15 | 14 | nn0zi 12642 |
. 2
⊢ ;14 ∈ ℤ |
| 16 | | 3nn0 12544 |
. . . 4
⊢ 3 ∈
ℕ0 |
| 17 | 2, 16 | deccl 12748 |
. . 3
⊢ ;13 ∈
ℕ0 |
| 18 | | 6nn0 12547 |
. . 3
⊢ 6 ∈
ℕ0 |
| 19 | 17, 18 | deccl 12748 |
. 2
⊢ ;;136 ∈ ℕ0 |
| 20 | | 8nn0 12549 |
. . . 4
⊢ 8 ∈
ℕ0 |
| 21 | 20, 11 | deccl 12748 |
. . 3
⊢ ;87 ∈
ℕ0 |
| 22 | | 0nn0 12541 |
. . 3
⊢ 0 ∈
ℕ0 |
| 23 | 21, 22 | deccl 12748 |
. 2
⊢ ;;870 ∈ ℕ0 |
| 24 | 1 | 1259lem1 17168 |
. 2
⊢
((2↑;17) mod 𝑁) = (;;136
mod 𝑁) |
| 25 | | eqid 2737 |
. . 3
⊢ ;17 = ;17 |
| 26 | | 2cn 12341 |
. . . . . 6
⊢ 2 ∈
ℂ |
| 27 | 26 | mulridi 11265 |
. . . . 5
⊢ (2
· 1) = 2 |
| 28 | 27 | oveq1i 7441 |
. . . 4
⊢ ((2
· 1) + 1) = (2 + 1) |
| 29 | | 2p1e3 12408 |
. . . 4
⊢ (2 + 1) =
3 |
| 30 | 28, 29 | eqtri 2765 |
. . 3
⊢ ((2
· 1) + 1) = 3 |
| 31 | | 7cn 12360 |
. . . 4
⊢ 7 ∈
ℂ |
| 32 | | 7t2e14 12842 |
. . . 4
⊢ (7
· 2) = ;14 |
| 33 | 31, 26, 32 | mulcomli 11270 |
. . 3
⊢ (2
· 7) = ;14 |
| 34 | 3, 2, 11, 25, 13, 2, 30, 33 | decmul2c 12799 |
. 2
⊢ (2
· ;17) = ;34 |
| 35 | | 9nn0 12550 |
. . . 4
⊢ 9 ∈
ℕ0 |
| 36 | | eqid 2737 |
. . . 4
⊢ ;;870 = ;;870 |
| 37 | | eqid 2737 |
. . . . 5
⊢ ;;125 = ;;125 |
| 38 | | eqid 2737 |
. . . . . 6
⊢ ;87 = ;87 |
| 39 | | eqid 2737 |
. . . . . 6
⊢ ;12 = ;12 |
| 40 | | 8p1e9 12416 |
. . . . . 6
⊢ (8 + 1) =
9 |
| 41 | | 7p2e9 12427 |
. . . . . 6
⊢ (7 + 2) =
9 |
| 42 | 20, 11, 2, 3, 38, 39, 40, 41 | decadd 12787 |
. . . . 5
⊢ (;87 + ;12) = ;99 |
| 43 | | 9p7e16 12825 |
. . . . . 6
⊢ (9 + 7) =
;16 |
| 44 | | eqid 2737 |
. . . . . . 7
⊢ ;14 = ;14 |
| 45 | | 3cn 12347 |
. . . . . . . . 9
⊢ 3 ∈
ℂ |
| 46 | | ax-1cn 11213 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
| 47 | | 3p1e4 12411 |
. . . . . . . . 9
⊢ (3 + 1) =
4 |
| 48 | 45, 46, 47 | addcomli 11453 |
. . . . . . . 8
⊢ (1 + 3) =
4 |
| 49 | 13 | dec0h 12755 |
. . . . . . . 8
⊢ 4 = ;04 |
| 50 | 48, 49 | eqtri 2765 |
. . . . . . 7
⊢ (1 + 3) =
;04 |
| 51 | 46 | mulridi 11265 |
. . . . . . . . 9
⊢ (1
· 1) = 1 |
| 52 | | 00id 11436 |
. . . . . . . . 9
⊢ (0 + 0) =
0 |
| 53 | 51, 52 | oveq12i 7443 |
. . . . . . . 8
⊢ ((1
· 1) + (0 + 0)) = (1 + 0) |
| 54 | 46 | addridi 11448 |
. . . . . . . 8
⊢ (1 + 0) =
1 |
| 55 | 53, 54 | eqtri 2765 |
. . . . . . 7
⊢ ((1
· 1) + (0 + 0)) = 1 |
| 56 | | 4cn 12351 |
. . . . . . . . . 10
⊢ 4 ∈
ℂ |
| 57 | 56 | mulridi 11265 |
. . . . . . . . 9
⊢ (4
· 1) = 4 |
| 58 | 57 | oveq1i 7441 |
. . . . . . . 8
⊢ ((4
· 1) + 4) = (4 + 4) |
| 59 | | 4p4e8 12421 |
. . . . . . . 8
⊢ (4 + 4) =
8 |
| 60 | 20 | dec0h 12755 |
. . . . . . . 8
⊢ 8 = ;08 |
| 61 | 58, 59, 60 | 3eqtri 2769 |
. . . . . . 7
⊢ ((4
· 1) + 4) = ;08 |
| 62 | 2, 13, 22, 13, 44, 50, 2, 20, 22, 55, 61 | decmac 12785 |
. . . . . 6
⊢ ((;14 · 1) + (1 + 3)) = ;18 |
| 63 | 18 | dec0h 12755 |
. . . . . . 7
⊢ 6 = ;06 |
| 64 | 26 | mullidi 11266 |
. . . . . . . . 9
⊢ (1
· 2) = 2 |
| 65 | 46 | addlidi 11449 |
. . . . . . . . 9
⊢ (0 + 1) =
1 |
| 66 | 64, 65 | oveq12i 7443 |
. . . . . . . 8
⊢ ((1
· 2) + (0 + 1)) = (2 + 1) |
| 67 | 66, 29 | eqtri 2765 |
. . . . . . 7
⊢ ((1
· 2) + (0 + 1)) = 3 |
| 68 | | 4t2e8 12434 |
. . . . . . . . 9
⊢ (4
· 2) = 8 |
| 69 | 68 | oveq1i 7441 |
. . . . . . . 8
⊢ ((4
· 2) + 6) = (8 + 6) |
| 70 | | 8p6e14 12817 |
. . . . . . . 8
⊢ (8 + 6) =
;14 |
| 71 | 69, 70 | eqtri 2765 |
. . . . . . 7
⊢ ((4
· 2) + 6) = ;14 |
| 72 | 2, 13, 22, 18, 44, 63, 3, 13, 2, 67, 71 | decmac 12785 |
. . . . . 6
⊢ ((;14 · 2) + 6) = ;34 |
| 73 | 2, 3, 2, 18, 39, 43, 14, 13, 16, 62, 72 | decma2c 12786 |
. . . . 5
⊢ ((;14 · ;12) + (9 + 7)) = ;;184 |
| 74 | 35 | dec0h 12755 |
. . . . . 6
⊢ 9 = ;09 |
| 75 | | 5cn 12354 |
. . . . . . . . 9
⊢ 5 ∈
ℂ |
| 76 | 75 | mullidi 11266 |
. . . . . . . 8
⊢ (1
· 5) = 5 |
| 77 | 26 | addlidi 11449 |
. . . . . . . 8
⊢ (0 + 2) =
2 |
| 78 | 76, 77 | oveq12i 7443 |
. . . . . . 7
⊢ ((1
· 5) + (0 + 2)) = (5 + 2) |
| 79 | | 5p2e7 12422 |
. . . . . . 7
⊢ (5 + 2) =
7 |
| 80 | 78, 79 | eqtri 2765 |
. . . . . 6
⊢ ((1
· 5) + (0 + 2)) = 7 |
| 81 | | 5t4e20 12835 |
. . . . . . . 8
⊢ (5
· 4) = ;20 |
| 82 | 75, 56, 81 | mulcomli 11270 |
. . . . . . 7
⊢ (4
· 5) = ;20 |
| 83 | | 9cn 12366 |
. . . . . . . 8
⊢ 9 ∈
ℂ |
| 84 | 83 | addlidi 11449 |
. . . . . . 7
⊢ (0 + 9) =
9 |
| 85 | 3, 22, 35, 82, 84 | decaddi 12793 |
. . . . . 6
⊢ ((4
· 5) + 9) = ;29 |
| 86 | 2, 13, 22, 35, 44, 74, 5, 35, 3, 80, 85 | decmac 12785 |
. . . . 5
⊢ ((;14 · 5) + 9) = ;79 |
| 87 | 4, 5, 35, 35, 37, 42, 14, 35, 11, 73, 86 | decma2c 12786 |
. . . 4
⊢ ((;14 · ;;125) +
(;87 + ;12)) = ;;;1849 |
| 88 | 83 | mullidi 11266 |
. . . . . . . . 9
⊢ (1
· 9) = 9 |
| 89 | 88 | oveq1i 7441 |
. . . . . . . 8
⊢ ((1
· 9) + 3) = (9 + 3) |
| 90 | | 9p3e12 12821 |
. . . . . . . 8
⊢ (9 + 3) =
;12 |
| 91 | 89, 90 | eqtri 2765 |
. . . . . . 7
⊢ ((1
· 9) + 3) = ;12 |
| 92 | | 9t4e36 12857 |
. . . . . . . 8
⊢ (9
· 4) = ;36 |
| 93 | 83, 56, 92 | mulcomli 11270 |
. . . . . . 7
⊢ (4
· 9) = ;36 |
| 94 | 35, 2, 13, 44, 18, 16, 91, 93 | decmul1c 12798 |
. . . . . 6
⊢ (;14 · 9) = ;;126 |
| 95 | 94 | oveq1i 7441 |
. . . . 5
⊢ ((;14 · 9) + 0) = (;;126 + 0) |
| 96 | 4, 18 | deccl 12748 |
. . . . . . 7
⊢ ;;126 ∈ ℕ0 |
| 97 | 96 | nn0cni 12538 |
. . . . . 6
⊢ ;;126 ∈ ℂ |
| 98 | 97 | addridi 11448 |
. . . . 5
⊢ (;;126 + 0) = ;;126 |
| 99 | 95, 98 | eqtri 2765 |
. . . 4
⊢ ((;14 · 9) + 0) = ;;126 |
| 100 | 6, 35, 21, 22, 1, 36, 14, 18, 4, 87, 99 | decma2c 12786 |
. . 3
⊢ ((;14 · 𝑁) + ;;870) =
;;;;18496 |
| 101 | | eqid 2737 |
. . . 4
⊢ ;;136 = ;;136 |
| 102 | 20, 2 | deccl 12748 |
. . . 4
⊢ ;81 ∈
ℕ0 |
| 103 | | eqid 2737 |
. . . . 5
⊢ ;13 = ;13 |
| 104 | | eqid 2737 |
. . . . 5
⊢ ;81 = ;81 |
| 105 | 13, 22 | deccl 12748 |
. . . . 5
⊢ ;40 ∈
ℕ0 |
| 106 | | eqid 2737 |
. . . . . . 7
⊢ ;40 = ;40 |
| 107 | 56 | addlidi 11449 |
. . . . . . 7
⊢ (0 + 4) =
4 |
| 108 | | 8cn 12363 |
. . . . . . . 8
⊢ 8 ∈
ℂ |
| 109 | 108 | addridi 11448 |
. . . . . . 7
⊢ (8 + 0) =
8 |
| 110 | 22, 20, 13, 22, 60, 106, 107, 109 | decadd 12787 |
. . . . . 6
⊢ (8 +
;40) = ;48 |
| 111 | | 4p1e5 12412 |
. . . . . . . 8
⊢ (4 + 1) =
5 |
| 112 | 5 | dec0h 12755 |
. . . . . . . 8
⊢ 5 = ;05 |
| 113 | 111, 112 | eqtri 2765 |
. . . . . . 7
⊢ (4 + 1) =
;05 |
| 114 | 45 | mulridi 11265 |
. . . . . . . . 9
⊢ (3
· 1) = 3 |
| 115 | 114 | oveq1i 7441 |
. . . . . . . 8
⊢ ((3
· 1) + 5) = (3 + 5) |
| 116 | | 5p3e8 12423 |
. . . . . . . . 9
⊢ (5 + 3) =
8 |
| 117 | 75, 45, 116 | addcomli 11453 |
. . . . . . . 8
⊢ (3 + 5) =
8 |
| 118 | 115, 117,
60 | 3eqtri 2769 |
. . . . . . 7
⊢ ((3
· 1) + 5) = ;08 |
| 119 | 2, 16, 22, 5, 103, 113, 2, 20, 22, 55, 118 | decmac 12785 |
. . . . . 6
⊢ ((;13 · 1) + (4 + 1)) = ;18 |
| 120 | | 6cn 12357 |
. . . . . . . . 9
⊢ 6 ∈
ℂ |
| 121 | 120 | mulridi 11265 |
. . . . . . . 8
⊢ (6
· 1) = 6 |
| 122 | 121 | oveq1i 7441 |
. . . . . . 7
⊢ ((6
· 1) + 8) = (6 + 8) |
| 123 | 108, 120,
70 | addcomli 11453 |
. . . . . . 7
⊢ (6 + 8) =
;14 |
| 124 | 122, 123 | eqtri 2765 |
. . . . . 6
⊢ ((6
· 1) + 8) = ;14 |
| 125 | 17, 18, 13, 20, 101, 110, 2, 13, 2, 119, 124 | decmac 12785 |
. . . . 5
⊢ ((;;136 · 1) + (8 + ;40)) = ;;184 |
| 126 | 2 | dec0h 12755 |
. . . . . 6
⊢ 1 = ;01 |
| 127 | 65, 126 | eqtri 2765 |
. . . . . . 7
⊢ (0 + 1) =
;01 |
| 128 | 45 | mullidi 11266 |
. . . . . . . . 9
⊢ (1
· 3) = 3 |
| 129 | 128, 65 | oveq12i 7443 |
. . . . . . . 8
⊢ ((1
· 3) + (0 + 1)) = (3 + 1) |
| 130 | 129, 47 | eqtri 2765 |
. . . . . . 7
⊢ ((1
· 3) + (0 + 1)) = 4 |
| 131 | | 3t3e9 12433 |
. . . . . . . . 9
⊢ (3
· 3) = 9 |
| 132 | 131 | oveq1i 7441 |
. . . . . . . 8
⊢ ((3
· 3) + 1) = (9 + 1) |
| 133 | | 9p1e10 12735 |
. . . . . . . 8
⊢ (9 + 1) =
;10 |
| 134 | 132, 133 | eqtri 2765 |
. . . . . . 7
⊢ ((3
· 3) + 1) = ;10 |
| 135 | 2, 16, 22, 2, 103, 127, 16, 22, 2, 130, 134 | decmac 12785 |
. . . . . 6
⊢ ((;13 · 3) + (0 + 1)) = ;40 |
| 136 | | 6t3e18 12838 |
. . . . . . 7
⊢ (6
· 3) = ;18 |
| 137 | 2, 20, 2, 136, 40 | decaddi 12793 |
. . . . . 6
⊢ ((6
· 3) + 1) = ;19 |
| 138 | 17, 18, 22, 2, 101, 126, 16, 35, 2, 135, 137 | decmac 12785 |
. . . . 5
⊢ ((;;136 · 3) + 1) = ;;409 |
| 139 | 2, 16, 20, 2, 103, 104, 19, 35, 105, 125, 138 | decma2c 12786 |
. . . 4
⊢ ((;;136 · ;13) + ;81) = ;;;1849 |
| 140 | 16 | dec0h 12755 |
. . . . . 6
⊢ 3 = ;03 |
| 141 | 120 | mullidi 11266 |
. . . . . . . 8
⊢ (1
· 6) = 6 |
| 142 | 141, 77 | oveq12i 7443 |
. . . . . . 7
⊢ ((1
· 6) + (0 + 2)) = (6 + 2) |
| 143 | | 6p2e8 12425 |
. . . . . . 7
⊢ (6 + 2) =
8 |
| 144 | 142, 143 | eqtri 2765 |
. . . . . 6
⊢ ((1
· 6) + (0 + 2)) = 8 |
| 145 | 120, 45, 136 | mulcomli 11270 |
. . . . . . 7
⊢ (3
· 6) = ;18 |
| 146 | | 1p1e2 12391 |
. . . . . . 7
⊢ (1 + 1) =
2 |
| 147 | | 8p3e11 12814 |
. . . . . . 7
⊢ (8 + 3) =
;11 |
| 148 | 2, 20, 16, 145, 146, 2, 147 | decaddci 12794 |
. . . . . 6
⊢ ((3
· 6) + 3) = ;21 |
| 149 | 2, 16, 22, 16, 103, 140, 18, 2, 3, 144, 148 | decmac 12785 |
. . . . 5
⊢ ((;13 · 6) + 3) = ;81 |
| 150 | | 6t6e36 12841 |
. . . . 5
⊢ (6
· 6) = ;36 |
| 151 | 18, 17, 18, 101, 18, 16, 149, 150 | decmul1c 12798 |
. . . 4
⊢ (;;136 · 6) = ;;816 |
| 152 | 19, 17, 18, 101, 18, 102, 139, 151 | decmul2c 12799 |
. . 3
⊢ (;;136 · ;;136) =
;;;;18496 |
| 153 | 100, 152 | eqtr4i 2768 |
. 2
⊢ ((;14 · 𝑁) + ;;870) =
(;;136 · ;;136) |
| 154 | 9, 10, 12, 15, 19, 23, 24, 34, 153 | mod2xi 17107 |
1
⊢
((2↑;34) mod 𝑁) = (;;870
mod 𝑁) |