Proof of Theorem 4001lem1
| Step | Hyp | Ref
| Expression |
| 1 | | 4001prm.1 |
. . 3
⊢ 𝑁 = ;;;4001 |
| 2 | | 4nn0 12545 |
. . . . . 6
⊢ 4 ∈
ℕ0 |
| 3 | | 0nn0 12541 |
. . . . . 6
⊢ 0 ∈
ℕ0 |
| 4 | 2, 3 | deccl 12748 |
. . . . 5
⊢ ;40 ∈
ℕ0 |
| 5 | 4, 3 | deccl 12748 |
. . . 4
⊢ ;;400 ∈ ℕ0 |
| 6 | | 1nn 12277 |
. . . 4
⊢ 1 ∈
ℕ |
| 7 | 5, 6 | decnncl 12753 |
. . 3
⊢ ;;;4001
∈ ℕ |
| 8 | 1, 7 | eqeltri 2837 |
. 2
⊢ 𝑁 ∈ ℕ |
| 9 | | 2nn 12339 |
. 2
⊢ 2 ∈
ℕ |
| 10 | | 10nn0 12751 |
. . 3
⊢ ;10 ∈
ℕ0 |
| 11 | 10, 3 | deccl 12748 |
. 2
⊢ ;;100 ∈ ℕ0 |
| 12 | | 9nn0 12550 |
. . . 4
⊢ 9 ∈
ℕ0 |
| 13 | 12, 2 | deccl 12748 |
. . 3
⊢ ;94 ∈
ℕ0 |
| 14 | 13 | nn0zi 12642 |
. 2
⊢ ;94 ∈ ℤ |
| 15 | | 6nn0 12547 |
. . . 4
⊢ 6 ∈
ℕ0 |
| 16 | | 1nn0 12542 |
. . . 4
⊢ 1 ∈
ℕ0 |
| 17 | 15, 16 | deccl 12748 |
. . 3
⊢ ;61 ∈
ℕ0 |
| 18 | 17, 2 | deccl 12748 |
. 2
⊢ ;;614 ∈ ℕ0 |
| 19 | 12, 3 | deccl 12748 |
. . 3
⊢ ;90 ∈
ℕ0 |
| 20 | | 2nn0 12543 |
. . 3
⊢ 2 ∈
ℕ0 |
| 21 | 19, 20 | deccl 12748 |
. 2
⊢ ;;902 ∈ ℕ0 |
| 22 | | 5nn0 12546 |
. . . 4
⊢ 5 ∈
ℕ0 |
| 23 | 22, 3 | deccl 12748 |
. . 3
⊢ ;50 ∈
ℕ0 |
| 24 | | 8nn0 12549 |
. . . . . 6
⊢ 8 ∈
ℕ0 |
| 25 | 20, 24 | deccl 12748 |
. . . . 5
⊢ ;28 ∈
ℕ0 |
| 26 | 25, 15 | deccl 12748 |
. . . 4
⊢ ;;286 ∈ ℕ0 |
| 27 | 26 | nn0zi 12642 |
. . 3
⊢ ;;286 ∈ ℤ |
| 28 | | 7nn0 12548 |
. . . . 5
⊢ 7 ∈
ℕ0 |
| 29 | 10, 28 | deccl 12748 |
. . . 4
⊢ ;;107 ∈ ℕ0 |
| 30 | 29, 3 | deccl 12748 |
. . 3
⊢ ;;;1070
∈ ℕ0 |
| 31 | 20, 22 | deccl 12748 |
. . . 4
⊢ ;25 ∈
ℕ0 |
| 32 | 10, 2 | deccl 12748 |
. . . . . 6
⊢ ;;104 ∈ ℕ0 |
| 33 | 32, 15 | deccl 12748 |
. . . . 5
⊢ ;;;1046
∈ ℕ0 |
| 34 | 33 | nn0zi 12642 |
. . . 4
⊢ ;;;1046
∈ ℤ |
| 35 | 20, 3 | deccl 12748 |
. . . . . 6
⊢ ;20 ∈
ℕ0 |
| 36 | 35, 2 | deccl 12748 |
. . . . 5
⊢ ;;204 ∈ ℕ0 |
| 37 | 36, 15 | deccl 12748 |
. . . 4
⊢ ;;;2046
∈ ℕ0 |
| 38 | 20, 2 | deccl 12748 |
. . . . 5
⊢ ;24 ∈
ℕ0 |
| 39 | | 0z 12624 |
. . . . 5
⊢ 0 ∈
ℤ |
| 40 | 10, 20 | deccl 12748 |
. . . . . 6
⊢ ;;102 ∈ ℕ0 |
| 41 | | 3nn0 12544 |
. . . . . 6
⊢ 3 ∈
ℕ0 |
| 42 | 40, 41 | deccl 12748 |
. . . . 5
⊢ ;;;1023
∈ ℕ0 |
| 43 | 16, 20 | deccl 12748 |
. . . . . 6
⊢ ;12 ∈
ℕ0 |
| 44 | | 2z 12649 |
. . . . . 6
⊢ 2 ∈
ℤ |
| 45 | 12, 22 | deccl 12748 |
. . . . . 6
⊢ ;95 ∈
ℕ0 |
| 46 | | 1z 12647 |
. . . . . . 7
⊢ 1 ∈
ℤ |
| 47 | 15, 2 | deccl 12748 |
. . . . . . 7
⊢ ;64 ∈
ℕ0 |
| 48 | | 2exp6 17124 |
. . . . . . . 8
⊢
(2↑6) = ;64 |
| 49 | 48 | oveq1i 7441 |
. . . . . . 7
⊢
((2↑6) mod 𝑁) =
(;64 mod 𝑁) |
| 50 | | 6cn 12357 |
. . . . . . . 8
⊢ 6 ∈
ℂ |
| 51 | | 2cn 12341 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
| 52 | | 6t2e12 12837 |
. . . . . . . 8
⊢ (6
· 2) = ;12 |
| 53 | 50, 51, 52 | mulcomli 11270 |
. . . . . . 7
⊢ (2
· 6) = ;12 |
| 54 | | eqid 2737 |
. . . . . . . . 9
⊢ ;95 = ;95 |
| 55 | | eqid 2737 |
. . . . . . . . . 10
⊢ ;;400 = ;;400 |
| 56 | | 9cn 12366 |
. . . . . . . . . . . 12
⊢ 9 ∈
ℂ |
| 57 | 56 | addridi 11448 |
. . . . . . . . . . 11
⊢ (9 + 0) =
9 |
| 58 | 12 | dec0h 12755 |
. . . . . . . . . . 11
⊢ 9 = ;09 |
| 59 | 57, 58 | eqtri 2765 |
. . . . . . . . . 10
⊢ (9 + 0) =
;09 |
| 60 | | eqid 2737 |
. . . . . . . . . . 11
⊢ ;40 = ;40 |
| 61 | | 00id 11436 |
. . . . . . . . . . . 12
⊢ (0 + 0) =
0 |
| 62 | 3 | dec0h 12755 |
. . . . . . . . . . . 12
⊢ 0 = ;00 |
| 63 | 61, 62 | eqtri 2765 |
. . . . . . . . . . 11
⊢ (0 + 0) =
;00 |
| 64 | | 4cn 12351 |
. . . . . . . . . . . . . 14
⊢ 4 ∈
ℂ |
| 65 | 64 | mullidi 11266 |
. . . . . . . . . . . . 13
⊢ (1
· 4) = 4 |
| 66 | 65, 61 | oveq12i 7443 |
. . . . . . . . . . . 12
⊢ ((1
· 4) + (0 + 0)) = (4 + 0) |
| 67 | 64 | addridi 11448 |
. . . . . . . . . . . 12
⊢ (4 + 0) =
4 |
| 68 | 66, 67 | eqtri 2765 |
. . . . . . . . . . 11
⊢ ((1
· 4) + (0 + 0)) = 4 |
| 69 | | ax-1cn 11213 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
| 70 | 69 | mul01i 11451 |
. . . . . . . . . . . . 13
⊢ (1
· 0) = 0 |
| 71 | 70 | oveq1i 7441 |
. . . . . . . . . . . 12
⊢ ((1
· 0) + 0) = (0 + 0) |
| 72 | 71, 61, 62 | 3eqtri 2769 |
. . . . . . . . . . 11
⊢ ((1
· 0) + 0) = ;00 |
| 73 | 2, 3, 3, 3, 60, 63, 16, 3, 3, 68, 72 | decma2c 12786 |
. . . . . . . . . 10
⊢ ((1
· ;40) + (0 + 0)) = ;40 |
| 74 | 70 | oveq1i 7441 |
. . . . . . . . . . 11
⊢ ((1
· 0) + 9) = (0 + 9) |
| 75 | 56 | addlidi 11449 |
. . . . . . . . . . 11
⊢ (0 + 9) =
9 |
| 76 | 74, 75, 58 | 3eqtri 2769 |
. . . . . . . . . 10
⊢ ((1
· 0) + 9) = ;09 |
| 77 | 4, 3, 3, 12, 55, 59, 16, 12, 3, 73, 76 | decma2c 12786 |
. . . . . . . . 9
⊢ ((1
· ;;400) + (9 + 0)) = ;;409 |
| 78 | 69 | mulridi 11265 |
. . . . . . . . . . 11
⊢ (1
· 1) = 1 |
| 79 | 78 | oveq1i 7441 |
. . . . . . . . . 10
⊢ ((1
· 1) + 5) = (1 + 5) |
| 80 | | 5cn 12354 |
. . . . . . . . . . 11
⊢ 5 ∈
ℂ |
| 81 | | 5p1e6 12413 |
. . . . . . . . . . 11
⊢ (5 + 1) =
6 |
| 82 | 80, 69, 81 | addcomli 11453 |
. . . . . . . . . 10
⊢ (1 + 5) =
6 |
| 83 | 15 | dec0h 12755 |
. . . . . . . . . 10
⊢ 6 = ;06 |
| 84 | 79, 82, 83 | 3eqtri 2769 |
. . . . . . . . 9
⊢ ((1
· 1) + 5) = ;06 |
| 85 | 5, 16, 12, 22, 1, 54, 16, 15, 3, 77, 84 | decma2c 12786 |
. . . . . . . 8
⊢ ((1
· 𝑁) + ;95) = ;;;4096 |
| 86 | | eqid 2737 |
. . . . . . . . 9
⊢ ;64 = ;64 |
| 87 | | eqid 2737 |
. . . . . . . . . 10
⊢ ;25 = ;25 |
| 88 | | 2p2e4 12401 |
. . . . . . . . . . . 12
⊢ (2 + 2) =
4 |
| 89 | 88 | oveq2i 7442 |
. . . . . . . . . . 11
⊢ ((6
· 6) + (2 + 2)) = ((6 · 6) + 4) |
| 90 | | 6t6e36 12841 |
. . . . . . . . . . . 12
⊢ (6
· 6) = ;36 |
| 91 | | 3p1e4 12411 |
. . . . . . . . . . . 12
⊢ (3 + 1) =
4 |
| 92 | | 6p4e10 12805 |
. . . . . . . . . . . 12
⊢ (6 + 4) =
;10 |
| 93 | 41, 15, 2, 90, 91, 92 | decaddci2 12795 |
. . . . . . . . . . 11
⊢ ((6
· 6) + 4) = ;40 |
| 94 | 89, 93 | eqtri 2765 |
. . . . . . . . . 10
⊢ ((6
· 6) + (2 + 2)) = ;40 |
| 95 | | 6t4e24 12839 |
. . . . . . . . . . . 12
⊢ (6
· 4) = ;24 |
| 96 | 50, 64, 95 | mulcomli 11270 |
. . . . . . . . . . 11
⊢ (4
· 6) = ;24 |
| 97 | | 5p4e9 12424 |
. . . . . . . . . . . 12
⊢ (5 + 4) =
9 |
| 98 | 80, 64, 97 | addcomli 11453 |
. . . . . . . . . . 11
⊢ (4 + 5) =
9 |
| 99 | 20, 2, 22, 96, 98 | decaddi 12793 |
. . . . . . . . . 10
⊢ ((4
· 6) + 5) = ;29 |
| 100 | 15, 2, 20, 22, 86, 87, 15, 12, 20, 94, 99 | decmac 12785 |
. . . . . . . . 9
⊢ ((;64 · 6) + ;25) = ;;409 |
| 101 | | 4p1e5 12412 |
. . . . . . . . . . 11
⊢ (4 + 1) =
5 |
| 102 | 20, 2, 101, 95 | decsuc 12764 |
. . . . . . . . . 10
⊢ ((6
· 4) + 1) = ;25 |
| 103 | | 4t4e16 12832 |
. . . . . . . . . 10
⊢ (4
· 4) = ;16 |
| 104 | 2, 15, 2, 86, 15, 16, 102, 103 | decmul1c 12798 |
. . . . . . . . 9
⊢ (;64 · 4) = ;;256 |
| 105 | 47, 15, 2, 86, 15, 31, 100, 104 | decmul2c 12799 |
. . . . . . . 8
⊢ (;64 · ;64) = ;;;4096 |
| 106 | 85, 105 | eqtr4i 2768 |
. . . . . . 7
⊢ ((1
· 𝑁) + ;95) = (;64 · ;64) |
| 107 | 8, 9, 15, 46, 47, 45, 49, 53, 106 | mod2xi 17107 |
. . . . . 6
⊢
((2↑;12) mod 𝑁) = (;95 mod 𝑁) |
| 108 | | eqid 2737 |
. . . . . . 7
⊢ ;12 = ;12 |
| 109 | 51 | mulridi 11265 |
. . . . . . . . 9
⊢ (2
· 1) = 2 |
| 110 | 109 | oveq1i 7441 |
. . . . . . . 8
⊢ ((2
· 1) + 0) = (2 + 0) |
| 111 | 51 | addridi 11448 |
. . . . . . . 8
⊢ (2 + 0) =
2 |
| 112 | 110, 111 | eqtri 2765 |
. . . . . . 7
⊢ ((2
· 1) + 0) = 2 |
| 113 | | 2t2e4 12430 |
. . . . . . . 8
⊢ (2
· 2) = 4 |
| 114 | 2 | dec0h 12755 |
. . . . . . . 8
⊢ 4 = ;04 |
| 115 | 113, 114 | eqtri 2765 |
. . . . . . 7
⊢ (2
· 2) = ;04 |
| 116 | 20, 16, 20, 108, 2, 3, 112, 115 | decmul2c 12799 |
. . . . . 6
⊢ (2
· ;12) = ;24 |
| 117 | | eqid 2737 |
. . . . . . . 8
⊢ ;;;1023 =
;;;1023 |
| 118 | 40 | nn0cni 12538 |
. . . . . . . . . 10
⊢ ;;102 ∈ ℂ |
| 119 | 118 | addridi 11448 |
. . . . . . . . 9
⊢ (;;102 + 0) = ;;102 |
| 120 | | dec10p 12776 |
. . . . . . . . . 10
⊢ (;10 + 0) = ;10 |
| 121 | | 4t2e8 12434 |
. . . . . . . . . . . . 13
⊢ (4
· 2) = 8 |
| 122 | 64, 51, 121 | mulcomli 11270 |
. . . . . . . . . . . 12
⊢ (2
· 4) = 8 |
| 123 | 69 | addridi 11448 |
. . . . . . . . . . . 12
⊢ (1 + 0) =
1 |
| 124 | 122, 123 | oveq12i 7443 |
. . . . . . . . . . 11
⊢ ((2
· 4) + (1 + 0)) = (8 + 1) |
| 125 | | 8p1e9 12416 |
. . . . . . . . . . 11
⊢ (8 + 1) =
9 |
| 126 | 124, 125 | eqtri 2765 |
. . . . . . . . . 10
⊢ ((2
· 4) + (1 + 0)) = 9 |
| 127 | 51 | mul01i 11451 |
. . . . . . . . . . . 12
⊢ (2
· 0) = 0 |
| 128 | 127 | oveq1i 7441 |
. . . . . . . . . . 11
⊢ ((2
· 0) + 0) = (0 + 0) |
| 129 | 128, 61, 62 | 3eqtri 2769 |
. . . . . . . . . 10
⊢ ((2
· 0) + 0) = ;00 |
| 130 | 2, 3, 16, 3, 60, 120, 20, 3, 3, 126, 129 | decma2c 12786 |
. . . . . . . . 9
⊢ ((2
· ;40) + (;10 + 0)) = ;90 |
| 131 | 127 | oveq1i 7441 |
. . . . . . . . . 10
⊢ ((2
· 0) + 2) = (0 + 2) |
| 132 | 51 | addlidi 11449 |
. . . . . . . . . 10
⊢ (0 + 2) =
2 |
| 133 | 20 | dec0h 12755 |
. . . . . . . . . 10
⊢ 2 = ;02 |
| 134 | 131, 132,
133 | 3eqtri 2769 |
. . . . . . . . 9
⊢ ((2
· 0) + 2) = ;02 |
| 135 | 4, 3, 10, 20, 55, 119, 20, 20, 3, 130, 134 | decma2c 12786 |
. . . . . . . 8
⊢ ((2
· ;;400) + (;;102 +
0)) = ;;902 |
| 136 | 109 | oveq1i 7441 |
. . . . . . . . 9
⊢ ((2
· 1) + 3) = (2 + 3) |
| 137 | | 3cn 12347 |
. . . . . . . . . 10
⊢ 3 ∈
ℂ |
| 138 | | 3p2e5 12417 |
. . . . . . . . . 10
⊢ (3 + 2) =
5 |
| 139 | 137, 51, 138 | addcomli 11453 |
. . . . . . . . 9
⊢ (2 + 3) =
5 |
| 140 | 22 | dec0h 12755 |
. . . . . . . . 9
⊢ 5 = ;05 |
| 141 | 136, 139,
140 | 3eqtri 2769 |
. . . . . . . 8
⊢ ((2
· 1) + 3) = ;05 |
| 142 | 5, 16, 40, 41, 1, 117, 20, 22, 3, 135, 141 | decma2c 12786 |
. . . . . . 7
⊢ ((2
· 𝑁) + ;;;1023)
= ;;;9025 |
| 143 | 2, 28 | deccl 12748 |
. . . . . . . 8
⊢ ;47 ∈
ℕ0 |
| 144 | | eqid 2737 |
. . . . . . . . 9
⊢ ;47 = ;47 |
| 145 | 98 | oveq2i 7442 |
. . . . . . . . . 10
⊢ ((9
· 9) + (4 + 5)) = ((9 · 9) + 9) |
| 146 | | 9t9e81 12862 |
. . . . . . . . . . 11
⊢ (9
· 9) = ;81 |
| 147 | | 9p1e10 12735 |
. . . . . . . . . . . 12
⊢ (9 + 1) =
;10 |
| 148 | 56, 69, 147 | addcomli 11453 |
. . . . . . . . . . 11
⊢ (1 + 9) =
;10 |
| 149 | 24, 16, 12, 146, 125, 148 | decaddci2 12795 |
. . . . . . . . . 10
⊢ ((9
· 9) + 9) = ;90 |
| 150 | 145, 149 | eqtri 2765 |
. . . . . . . . 9
⊢ ((9
· 9) + (4 + 5)) = ;90 |
| 151 | | 9t5e45 12858 |
. . . . . . . . . . 11
⊢ (9
· 5) = ;45 |
| 152 | 56, 80, 151 | mulcomli 11270 |
. . . . . . . . . 10
⊢ (5
· 9) = ;45 |
| 153 | | 7cn 12360 |
. . . . . . . . . . 11
⊢ 7 ∈
ℂ |
| 154 | | 7p5e12 12810 |
. . . . . . . . . . 11
⊢ (7 + 5) =
;12 |
| 155 | 153, 80, 154 | addcomli 11453 |
. . . . . . . . . 10
⊢ (5 + 7) =
;12 |
| 156 | 2, 22, 28, 152, 101, 20, 155 | decaddci 12794 |
. . . . . . . . 9
⊢ ((5
· 9) + 7) = ;52 |
| 157 | 12, 22, 2, 28, 54, 144, 12, 20, 22, 150, 156 | decmac 12785 |
. . . . . . . 8
⊢ ((;95 · 9) + ;47) = ;;902 |
| 158 | | 5p2e7 12422 |
. . . . . . . . . 10
⊢ (5 + 2) =
7 |
| 159 | 2, 22, 20, 151, 158 | decaddi 12793 |
. . . . . . . . 9
⊢ ((9
· 5) + 2) = ;47 |
| 160 | | 5t5e25 12836 |
. . . . . . . . 9
⊢ (5
· 5) = ;25 |
| 161 | 22, 12, 22, 54, 22, 20, 159, 160 | decmul1c 12798 |
. . . . . . . 8
⊢ (;95 · 5) = ;;475 |
| 162 | 45, 12, 22, 54, 22, 143, 157, 161 | decmul2c 12799 |
. . . . . . 7
⊢ (;95 · ;95) = ;;;9025 |
| 163 | 142, 162 | eqtr4i 2768 |
. . . . . 6
⊢ ((2
· 𝑁) + ;;;1023)
= (;95 · ;95) |
| 164 | 8, 9, 43, 44, 45, 42, 107, 116, 163 | mod2xi 17107 |
. . . . 5
⊢
((2↑;24) mod 𝑁) = (;;;1023 mod 𝑁) |
| 165 | | eqid 2737 |
. . . . . 6
⊢ ;24 = ;24 |
| 166 | 20, 2, 101, 165 | decsuc 12764 |
. . . . 5
⊢ (;24 + 1) = ;25 |
| 167 | 37 | nn0cni 12538 |
. . . . . . 7
⊢ ;;;2046
∈ ℂ |
| 168 | 167 | addlidi 11449 |
. . . . . 6
⊢ (0 +
;;;2046)
= ;;;2046 |
| 169 | 8 | nncni 12276 |
. . . . . . . 8
⊢ 𝑁 ∈ ℂ |
| 170 | 169 | mul02i 11450 |
. . . . . . 7
⊢ (0
· 𝑁) =
0 |
| 171 | 170 | oveq1i 7441 |
. . . . . 6
⊢ ((0
· 𝑁) + ;;;2046)
= (0 + ;;;2046) |
| 172 | | eqid 2737 |
. . . . . . . 8
⊢ ;;102 = ;;102 |
| 173 | 20 | dec0u 12754 |
. . . . . . . 8
⊢ (;10 · 2) = ;20 |
| 174 | 20, 10, 20, 172, 173, 113 | decmul1 12797 |
. . . . . . 7
⊢ (;;102 · 2) = ;;204 |
| 175 | | 3t2e6 12432 |
. . . . . . 7
⊢ (3
· 2) = 6 |
| 176 | 20, 40, 41, 117, 174, 175 | decmul1 12797 |
. . . . . 6
⊢ (;;;1023
· 2) = ;;;2046 |
| 177 | 168, 171,
176 | 3eqtr4i 2775 |
. . . . 5
⊢ ((0
· 𝑁) + ;;;2046)
= (;;;1023
· 2) |
| 178 | 8, 9, 38, 39, 42, 37, 164, 166, 177 | modxp1i 17108 |
. . . 4
⊢
((2↑;25) mod 𝑁) = (;;;2046 mod 𝑁) |
| 179 | 113 | oveq1i 7441 |
. . . . . 6
⊢ ((2
· 2) + 1) = (4 + 1) |
| 180 | 179, 101 | eqtri 2765 |
. . . . 5
⊢ ((2
· 2) + 1) = 5 |
| 181 | | 5t2e10 12833 |
. . . . . 6
⊢ (5
· 2) = ;10 |
| 182 | 80, 51, 181 | mulcomli 11270 |
. . . . 5
⊢ (2
· 5) = ;10 |
| 183 | 20, 20, 22, 87, 3, 16, 180, 182 | decmul2c 12799 |
. . . 4
⊢ (2
· ;25) = ;50 |
| 184 | | eqid 2737 |
. . . . . 6
⊢ ;;;1070 =
;;;1070 |
| 185 | 20, 16 | deccl 12748 |
. . . . . . 7
⊢ ;21 ∈
ℕ0 |
| 186 | | eqid 2737 |
. . . . . . . 8
⊢ ;;107 = ;;107 |
| 187 | | eqid 2737 |
. . . . . . . 8
⊢ ;;104 = ;;104 |
| 188 | | 0p1e1 12388 |
. . . . . . . . 9
⊢ (0 + 1) =
1 |
| 189 | | 10p10e20 12828 |
. . . . . . . . 9
⊢ (;10 + ;10) = ;20 |
| 190 | 20, 3, 188, 189 | decsuc 12764 |
. . . . . . . 8
⊢ ((;10 + ;10) + 1) = ;21 |
| 191 | | 7p4e11 12809 |
. . . . . . . 8
⊢ (7 + 4) =
;11 |
| 192 | 10, 28, 10, 2, 186, 187, 190, 16, 191 | decaddc 12788 |
. . . . . . 7
⊢ (;;107 + ;;104) =
;;211 |
| 193 | 185 | nn0cni 12538 |
. . . . . . . . 9
⊢ ;21 ∈ ℂ |
| 194 | 193 | addridi 11448 |
. . . . . . . 8
⊢ (;21 + 0) = ;21 |
| 195 | 111, 20 | eqeltri 2837 |
. . . . . . . . 9
⊢ (2 + 0)
∈ ℕ0 |
| 196 | | eqid 2737 |
. . . . . . . . 9
⊢ ;;;1046 =
;;;1046 |
| 197 | | dfdec10 12736 |
. . . . . . . . . . 11
⊢ ;41 = ((;10 · 4) + 1) |
| 198 | 197 | eqcomi 2746 |
. . . . . . . . . 10
⊢ ((;10 · 4) + 1) = ;41 |
| 199 | | 6p2e8 12425 |
. . . . . . . . . . 11
⊢ (6 + 2) =
8 |
| 200 | 16, 15, 20, 103, 199 | decaddi 12793 |
. . . . . . . . . 10
⊢ ((4
· 4) + 2) = ;18 |
| 201 | 10, 2, 20, 187, 2, 24, 16, 198, 200 | decrmac 12791 |
. . . . . . . . 9
⊢ ((;;104 · 4) + 2) = ;;418 |
| 202 | 95, 111 | oveq12i 7443 |
. . . . . . . . . 10
⊢ ((6
· 4) + (2 + 0)) = (;24 +
2) |
| 203 | | 4p2e6 12419 |
. . . . . . . . . . 11
⊢ (4 + 2) =
6 |
| 204 | 20, 2, 20, 165, 203 | decaddi 12793 |
. . . . . . . . . 10
⊢ (;24 + 2) = ;26 |
| 205 | 202, 204 | eqtri 2765 |
. . . . . . . . 9
⊢ ((6
· 4) + (2 + 0)) = ;26 |
| 206 | 32, 15, 195, 196, 2, 15, 20, 201, 205 | decrmac 12791 |
. . . . . . . 8
⊢ ((;;;1046
· 4) + (2 + 0)) = ;;;4186 |
| 207 | 33 | nn0cni 12538 |
. . . . . . . . . . 11
⊢ ;;;1046
∈ ℂ |
| 208 | 207 | mul01i 11451 |
. . . . . . . . . 10
⊢ (;;;1046
· 0) = 0 |
| 209 | 208 | oveq1i 7441 |
. . . . . . . . 9
⊢ ((;;;1046
· 0) + 1) = (0 + 1) |
| 210 | 16 | dec0h 12755 |
. . . . . . . . 9
⊢ 1 = ;01 |
| 211 | 209, 188,
210 | 3eqtri 2769 |
. . . . . . . 8
⊢ ((;;;1046
· 0) + 1) = ;01 |
| 212 | 2, 3, 20, 16, 60, 194, 33, 16, 3, 206, 211 | decma2c 12786 |
. . . . . . 7
⊢ ((;;;1046
· ;40) + (;21 + 0)) = ;;;;41861 |
| 213 | 4, 3, 185, 16, 55, 192, 33, 16, 3, 212, 211 | decma2c 12786 |
. . . . . 6
⊢ ((;;;1046
· ;;400) + (;;107 +
;;104)) = ;;;;;418611 |
| 214 | 207 | mulridi 11265 |
. . . . . . . 8
⊢ (;;;1046
· 1) = ;;;1046 |
| 215 | 214 | oveq1i 7441 |
. . . . . . 7
⊢ ((;;;1046
· 1) + 0) = (;;;1046 + 0) |
| 216 | 207 | addridi 11448 |
. . . . . . 7
⊢ (;;;1046 +
0) = ;;;1046 |
| 217 | 215, 216 | eqtri 2765 |
. . . . . 6
⊢ ((;;;1046
· 1) + 0) = ;;;1046 |
| 218 | 5, 16, 29, 3, 1, 184, 33, 15, 32, 213, 217 | decma2c 12786 |
. . . . 5
⊢ ((;;;1046
· 𝑁) + ;;;1070)
= ;;;;;;4186116 |
| 219 | | eqid 2737 |
. . . . . 6
⊢ ;;;2046 =
;;;2046 |
| 220 | 43, 20 | deccl 12748 |
. . . . . . 7
⊢ ;;122 ∈ ℕ0 |
| 221 | 220, 28 | deccl 12748 |
. . . . . 6
⊢ ;;;1227
∈ ℕ0 |
| 222 | | eqid 2737 |
. . . . . . 7
⊢ ;;204 = ;;204 |
| 223 | | eqid 2737 |
. . . . . . 7
⊢ ;;;1227 =
;;;1227 |
| 224 | 24, 16 | deccl 12748 |
. . . . . . . 8
⊢ ;81 ∈
ℕ0 |
| 225 | 224, 12 | deccl 12748 |
. . . . . . 7
⊢ ;;819 ∈ ℕ0 |
| 226 | | eqid 2737 |
. . . . . . . 8
⊢ ;20 = ;20 |
| 227 | | eqid 2737 |
. . . . . . . . 9
⊢ ;;122 = ;;122 |
| 228 | | eqid 2737 |
. . . . . . . . 9
⊢ ;;819 = ;;819 |
| 229 | | eqid 2737 |
. . . . . . . . . . 11
⊢ ;81 = ;81 |
| 230 | | 8cn 12363 |
. . . . . . . . . . . 12
⊢ 8 ∈
ℂ |
| 231 | 230, 69, 125 | addcomli 11453 |
. . . . . . . . . . 11
⊢ (1 + 8) =
9 |
| 232 | | 2p1e3 12408 |
. . . . . . . . . . 11
⊢ (2 + 1) =
3 |
| 233 | 16, 20, 24, 16, 108, 229, 231, 232 | decadd 12787 |
. . . . . . . . . 10
⊢ (;12 + ;81) = ;93 |
| 234 | 12, 41, 91, 233 | decsuc 12764 |
. . . . . . . . 9
⊢ ((;12 + ;81) + 1) = ;94 |
| 235 | | 9p2e11 12820 |
. . . . . . . . . 10
⊢ (9 + 2) =
;11 |
| 236 | 56, 51, 235 | addcomli 11453 |
. . . . . . . . 9
⊢ (2 + 9) =
;11 |
| 237 | 43, 20, 224, 12, 227, 228, 234, 16, 236 | decaddc 12788 |
. . . . . . . 8
⊢ (;;122 + ;;819) =
;;941 |
| 238 | 13 | nn0cni 12538 |
. . . . . . . . . 10
⊢ ;94 ∈ ℂ |
| 239 | 238 | addridi 11448 |
. . . . . . . . 9
⊢ (;94 + 0) = ;94 |
| 240 | 123, 16 | eqeltri 2837 |
. . . . . . . . . . 11
⊢ (1 + 0)
∈ ℕ0 |
| 241 | 51 | mul02i 11450 |
. . . . . . . . . . . . 13
⊢ (0
· 2) = 0 |
| 242 | 241, 123 | oveq12i 7443 |
. . . . . . . . . . . 12
⊢ ((0
· 2) + (1 + 0)) = (0 + 1) |
| 243 | 242, 188 | eqtri 2765 |
. . . . . . . . . . 11
⊢ ((0
· 2) + (1 + 0)) = 1 |
| 244 | 20, 3, 240, 226, 20, 113, 243 | decrmanc 12790 |
. . . . . . . . . 10
⊢ ((;20 · 2) + (1 + 0)) = ;41 |
| 245 | 121 | oveq1i 7441 |
. . . . . . . . . . 11
⊢ ((4
· 2) + 0) = (8 + 0) |
| 246 | 230 | addridi 11448 |
. . . . . . . . . . 11
⊢ (8 + 0) =
8 |
| 247 | 24 | dec0h 12755 |
. . . . . . . . . . 11
⊢ 8 = ;08 |
| 248 | 245, 246,
247 | 3eqtri 2769 |
. . . . . . . . . 10
⊢ ((4
· 2) + 0) = ;08 |
| 249 | 35, 2, 16, 3, 222, 147, 20, 24, 3, 244, 248 | decmac 12785 |
. . . . . . . . 9
⊢ ((;;204 · 2) + (9 + 1)) = ;;418 |
| 250 | 64, 51, 203 | addcomli 11453 |
. . . . . . . . . 10
⊢ (2 + 4) =
6 |
| 251 | 16, 20, 2, 52, 250 | decaddi 12793 |
. . . . . . . . 9
⊢ ((6
· 2) + 4) = ;16 |
| 252 | 36, 15, 12, 2, 219, 239, 20, 15, 16, 249, 251 | decmac 12785 |
. . . . . . . 8
⊢ ((;;;2046
· 2) + (;94 + 0)) = ;;;4186 |
| 253 | 167 | mul01i 11451 |
. . . . . . . . . 10
⊢ (;;;2046
· 0) = 0 |
| 254 | 253 | oveq1i 7441 |
. . . . . . . . 9
⊢ ((;;;2046
· 0) + 1) = (0 + 1) |
| 255 | 254, 188,
210 | 3eqtri 2769 |
. . . . . . . 8
⊢ ((;;;2046
· 0) + 1) = ;01 |
| 256 | 20, 3, 13, 16, 226, 237, 37, 16, 3, 252, 255 | decma2c 12786 |
. . . . . . 7
⊢ ((;;;2046
· ;20) + (;;122 + ;;819))
= ;;;;41861 |
| 257 | 41 | dec0h 12755 |
. . . . . . . . 9
⊢ 3 = ;03 |
| 258 | 188, 16 | eqeltri 2837 |
. . . . . . . . . 10
⊢ (0 + 1)
∈ ℕ0 |
| 259 | 64 | mul02i 11450 |
. . . . . . . . . . . 12
⊢ (0
· 4) = 0 |
| 260 | 259, 188 | oveq12i 7443 |
. . . . . . . . . . 11
⊢ ((0
· 4) + (0 + 1)) = (0 + 1) |
| 261 | 260, 188 | eqtri 2765 |
. . . . . . . . . 10
⊢ ((0
· 4) + (0 + 1)) = 1 |
| 262 | 20, 3, 258, 226, 2, 122, 261 | decrmanc 12790 |
. . . . . . . . 9
⊢ ((;20 · 4) + (0 + 1)) = ;81 |
| 263 | | 6p3e9 12426 |
. . . . . . . . . 10
⊢ (6 + 3) =
9 |
| 264 | 16, 15, 41, 103, 263 | decaddi 12793 |
. . . . . . . . 9
⊢ ((4
· 4) + 3) = ;19 |
| 265 | 35, 2, 3, 41, 222, 257, 2, 12, 16, 262, 264 | decmac 12785 |
. . . . . . . 8
⊢ ((;;204 · 4) + 3) = ;;819 |
| 266 | 153, 64, 191 | addcomli 11453 |
. . . . . . . . 9
⊢ (4 + 7) =
;11 |
| 267 | 20, 2, 28, 95, 232, 16, 266 | decaddci 12794 |
. . . . . . . 8
⊢ ((6
· 4) + 7) = ;31 |
| 268 | 36, 15, 28, 219, 2, 16, 41, 265, 267 | decrmac 12791 |
. . . . . . 7
⊢ ((;;;2046
· 4) + 7) = ;;;8191 |
| 269 | 35, 2, 220, 28, 222, 223, 37, 16, 225, 256, 268 | decma2c 12786 |
. . . . . 6
⊢ ((;;;2046
· ;;204) + ;;;1227) = ;;;;;418611 |
| 270 | 50 | mul02i 11450 |
. . . . . . . . . . 11
⊢ (0
· 6) = 0 |
| 271 | 270 | oveq1i 7441 |
. . . . . . . . . 10
⊢ ((0
· 6) + 2) = (0 + 2) |
| 272 | 271, 132 | eqtri 2765 |
. . . . . . . . 9
⊢ ((0
· 6) + 2) = 2 |
| 273 | 20, 3, 20, 226, 15, 53, 272 | decrmanc 12790 |
. . . . . . . 8
⊢ ((;20 · 6) + 2) = ;;122 |
| 274 | | 4p3e7 12420 |
. . . . . . . . 9
⊢ (4 + 3) =
7 |
| 275 | 20, 2, 41, 96, 274 | decaddi 12793 |
. . . . . . . 8
⊢ ((4
· 6) + 3) = ;27 |
| 276 | 35, 2, 41, 222, 15, 28, 20, 273, 275 | decrmac 12791 |
. . . . . . 7
⊢ ((;;204 · 6) + 3) = ;;;1227 |
| 277 | 15, 36, 15, 219, 15, 41, 276, 90 | decmul1c 12798 |
. . . . . 6
⊢ (;;;2046
· 6) = ;;;;12276 |
| 278 | 37, 36, 15, 219, 15, 221, 269, 277 | decmul2c 12799 |
. . . . 5
⊢ (;;;2046
· ;;;2046)
= ;;;;;;4186116 |
| 279 | 218, 278 | eqtr4i 2768 |
. . . 4
⊢ ((;;;1046
· 𝑁) + ;;;1070)
= (;;;2046
· ;;;2046) |
| 280 | 8, 9, 31, 34, 37, 30, 178, 183, 279 | mod2xi 17107 |
. . 3
⊢
((2↑;50) mod 𝑁) = (;;;1070 mod 𝑁) |
| 281 | 23 | nn0cni 12538 |
. . . 4
⊢ ;50 ∈ ℂ |
| 282 | | eqid 2737 |
. . . . 5
⊢ ;50 = ;50 |
| 283 | 20, 22, 3, 282, 181, 241 | decmul1 12797 |
. . . 4
⊢ (;50 · 2) = ;;100 |
| 284 | 281, 51, 283 | mulcomli 11270 |
. . 3
⊢ (2
· ;50) = ;;100 |
| 285 | | eqid 2737 |
. . . . 5
⊢ ;;614 = ;;614 |
| 286 | 20, 12 | deccl 12748 |
. . . . 5
⊢ ;29 ∈
ℕ0 |
| 287 | | eqid 2737 |
. . . . . . 7
⊢ ;61 = ;61 |
| 288 | | eqid 2737 |
. . . . . . 7
⊢ ;29 = ;29 |
| 289 | 199 | oveq1i 7441 |
. . . . . . . 8
⊢ ((6 + 2)
+ 1) = (8 + 1) |
| 290 | 289, 125 | eqtri 2765 |
. . . . . . 7
⊢ ((6 + 2)
+ 1) = 9 |
| 291 | 15, 16, 20, 12, 287, 288, 290, 148 | decaddc2 12789 |
. . . . . 6
⊢ (;61 + ;29) = ;90 |
| 292 | 61, 3 | eqeltri 2837 |
. . . . . . . 8
⊢ (0 + 0)
∈ ℕ0 |
| 293 | | eqid 2737 |
. . . . . . . 8
⊢ ;;286 = ;;286 |
| 294 | | eqid 2737 |
. . . . . . . . 9
⊢ ;28 = ;28 |
| 295 | 122 | oveq1i 7441 |
. . . . . . . . . 10
⊢ ((2
· 4) + 3) = (8 + 3) |
| 296 | | 8p3e11 12814 |
. . . . . . . . . 10
⊢ (8 + 3) =
;11 |
| 297 | 295, 296 | eqtri 2765 |
. . . . . . . . 9
⊢ ((2
· 4) + 3) = ;11 |
| 298 | | 8t4e32 12850 |
. . . . . . . . . 10
⊢ (8
· 4) = ;32 |
| 299 | 41, 20, 20, 298, 88 | decaddi 12793 |
. . . . . . . . 9
⊢ ((8
· 4) + 2) = ;34 |
| 300 | 20, 24, 20, 294, 2, 2, 41, 297, 299 | decrmac 12791 |
. . . . . . . 8
⊢ ((;28 · 4) + 2) = ;;114 |
| 301 | 95, 61 | oveq12i 7443 |
. . . . . . . . 9
⊢ ((6
· 4) + (0 + 0)) = (;24 +
0) |
| 302 | 38 | nn0cni 12538 |
. . . . . . . . . 10
⊢ ;24 ∈ ℂ |
| 303 | 302 | addridi 11448 |
. . . . . . . . 9
⊢ (;24 + 0) = ;24 |
| 304 | 301, 303 | eqtri 2765 |
. . . . . . . 8
⊢ ((6
· 4) + (0 + 0)) = ;24 |
| 305 | 25, 15, 292, 293, 2, 2, 20, 300, 304 | decrmac 12791 |
. . . . . . 7
⊢ ((;;286 · 4) + (0 + 0)) = ;;;1144 |
| 306 | 26 | nn0cni 12538 |
. . . . . . . . . 10
⊢ ;;286 ∈ ℂ |
| 307 | 306 | mul01i 11451 |
. . . . . . . . 9
⊢ (;;286 · 0) = 0 |
| 308 | 307 | oveq1i 7441 |
. . . . . . . 8
⊢ ((;;286 · 0) + 9) = (0 + 9) |
| 309 | 308, 75, 58 | 3eqtri 2769 |
. . . . . . 7
⊢ ((;;286 · 0) + 9) = ;09 |
| 310 | 2, 3, 3, 12, 60, 59, 26, 12, 3, 305, 309 | decma2c 12786 |
. . . . . 6
⊢ ((;;286 · ;40) + (9 + 0)) = ;;;;11449 |
| 311 | 307 | oveq1i 7441 |
. . . . . . 7
⊢ ((;;286 · 0) + 0) = (0 + 0) |
| 312 | 311, 61, 62 | 3eqtri 2769 |
. . . . . 6
⊢ ((;;286 · 0) + 0) = ;00 |
| 313 | 4, 3, 12, 3, 55, 291, 26, 3, 3, 310, 312 | decma2c 12786 |
. . . . 5
⊢ ((;;286 · ;;400) +
(;61 + ;29)) = ;;;;;114490 |
| 314 | 230 | mulridi 11265 |
. . . . . . . 8
⊢ (8
· 1) = 8 |
| 315 | 16, 20, 24, 294, 109, 314 | decmul1 12797 |
. . . . . . 7
⊢ (;28 · 1) = ;28 |
| 316 | 20, 24, 125, 315 | decsuc 12764 |
. . . . . 6
⊢ ((;28 · 1) + 1) = ;29 |
| 317 | 50 | mulridi 11265 |
. . . . . . . 8
⊢ (6
· 1) = 6 |
| 318 | 317 | oveq1i 7441 |
. . . . . . 7
⊢ ((6
· 1) + 4) = (6 + 4) |
| 319 | 318, 92 | eqtri 2765 |
. . . . . 6
⊢ ((6
· 1) + 4) = ;10 |
| 320 | 25, 15, 2, 293, 16, 3, 16, 316, 319 | decrmac 12791 |
. . . . 5
⊢ ((;;286 · 1) + 4) = ;;290 |
| 321 | 5, 16, 17, 2, 1, 285, 26, 3, 286, 313, 320 | decma2c 12786 |
. . . 4
⊢ ((;;286 · 𝑁) + ;;614) =
;;;;;;1144900 |
| 322 | 16, 16 | deccl 12748 |
. . . . . . . . 9
⊢ ;11 ∈
ℕ0 |
| 323 | 322, 2 | deccl 12748 |
. . . . . . . 8
⊢ ;;114 ∈ ℕ0 |
| 324 | 323, 2 | deccl 12748 |
. . . . . . 7
⊢ ;;;1144
∈ ℕ0 |
| 325 | 324, 12 | deccl 12748 |
. . . . . 6
⊢ ;;;;11449 ∈
ℕ0 |
| 326 | 28, 2 | deccl 12748 |
. . . . . . . 8
⊢ ;74 ∈
ℕ0 |
| 327 | 326, 12 | deccl 12748 |
. . . . . . 7
⊢ ;;749 ∈ ℕ0 |
| 328 | | eqid 2737 |
. . . . . . . 8
⊢ ;10 = ;10 |
| 329 | | eqid 2737 |
. . . . . . . 8
⊢ ;;749 = ;;749 |
| 330 | 326 | nn0cni 12538 |
. . . . . . . . . 10
⊢ ;74 ∈ ℂ |
| 331 | 330 | addridi 11448 |
. . . . . . . . 9
⊢ (;74 + 0) = ;74 |
| 332 | 153 | addridi 11448 |
. . . . . . . . . . 11
⊢ (7 + 0) =
7 |
| 333 | 332, 28 | eqeltri 2837 |
. . . . . . . . . 10
⊢ (7 + 0)
∈ ℕ0 |
| 334 | 10 | nn0cni 12538 |
. . . . . . . . . . . 12
⊢ ;10 ∈ ℂ |
| 335 | 334 | mulridi 11265 |
. . . . . . . . . . 11
⊢ (;10 · 1) = ;10 |
| 336 | 16, 3, 188, 335 | decsuc 12764 |
. . . . . . . . . 10
⊢ ((;10 · 1) + 1) = ;11 |
| 337 | 153 | mulridi 11265 |
. . . . . . . . . . . 12
⊢ (7
· 1) = 7 |
| 338 | 337, 332 | oveq12i 7443 |
. . . . . . . . . . 11
⊢ ((7
· 1) + (7 + 0)) = (7 + 7) |
| 339 | | 7p7e14 12812 |
. . . . . . . . . . 11
⊢ (7 + 7) =
;14 |
| 340 | 338, 339 | eqtri 2765 |
. . . . . . . . . 10
⊢ ((7
· 1) + (7 + 0)) = ;14 |
| 341 | 10, 28, 333, 186, 16, 2, 16, 336, 340 | decrmac 12791 |
. . . . . . . . 9
⊢ ((;;107 · 1) + (7 + 0)) = ;;114 |
| 342 | 69 | mul02i 11450 |
. . . . . . . . . . 11
⊢ (0
· 1) = 0 |
| 343 | 342 | oveq1i 7441 |
. . . . . . . . . 10
⊢ ((0
· 1) + 4) = (0 + 4) |
| 344 | 64 | addlidi 11449 |
. . . . . . . . . 10
⊢ (0 + 4) =
4 |
| 345 | 343, 344,
114 | 3eqtri 2769 |
. . . . . . . . 9
⊢ ((0
· 1) + 4) = ;04 |
| 346 | 29, 3, 28, 2, 184, 331, 16, 2, 3, 341, 345 | decmac 12785 |
. . . . . . . 8
⊢ ((;;;1070
· 1) + (;74 + 0)) = ;;;1144 |
| 347 | 30 | nn0cni 12538 |
. . . . . . . . . . 11
⊢ ;;;1070
∈ ℂ |
| 348 | 347 | mul01i 11451 |
. . . . . . . . . 10
⊢ (;;;1070
· 0) = 0 |
| 349 | 348 | oveq1i 7441 |
. . . . . . . . 9
⊢ ((;;;1070
· 0) + 9) = (0 + 9) |
| 350 | 349, 75, 58 | 3eqtri 2769 |
. . . . . . . 8
⊢ ((;;;1070
· 0) + 9) = ;09 |
| 351 | 16, 3, 326, 12, 328, 329, 30, 12, 3, 346, 350 | decma2c 12786 |
. . . . . . 7
⊢ ((;;;1070
· ;10) + ;;749) =
;;;;11449 |
| 352 | | dfdec10 12736 |
. . . . . . . . . 10
⊢ ;74 = ((;10 · 7) + 4) |
| 353 | 352 | eqcomi 2746 |
. . . . . . . . 9
⊢ ((;10 · 7) + 4) = ;74 |
| 354 | | 7t7e49 12847 |
. . . . . . . . 9
⊢ (7
· 7) = ;49 |
| 355 | 28, 10, 28, 186, 12, 2, 353, 354 | decmul1c 12798 |
. . . . . . . 8
⊢ (;;107 · 7) = ;;749 |
| 356 | 153 | mul02i 11450 |
. . . . . . . 8
⊢ (0
· 7) = 0 |
| 357 | 28, 29, 3, 184, 355, 356 | decmul1 12797 |
. . . . . . 7
⊢ (;;;1070
· 7) = ;;;7490 |
| 358 | 30, 10, 28, 186, 3, 327, 351, 357 | decmul2c 12799 |
. . . . . 6
⊢ (;;;1070
· ;;107) = ;;;;;114490 |
| 359 | 325, 3, 3, 358, 61 | decaddi 12793 |
. . . . 5
⊢ ((;;;1070
· ;;107) + 0) = ;;;;;114490 |
| 360 | 348, 62 | eqtri 2765 |
. . . . 5
⊢ (;;;1070
· 0) = ;00 |
| 361 | 30, 29, 3, 184, 3, 3, 359, 360 | decmul2c 12799 |
. . . 4
⊢ (;;;1070
· ;;;1070)
= ;;;;;;1144900 |
| 362 | 321, 361 | eqtr4i 2768 |
. . 3
⊢ ((;;286 · 𝑁) + ;;614) =
(;;;1070
· ;;;1070) |
| 363 | 8, 9, 23, 27, 30, 18, 280, 284, 362 | mod2xi 17107 |
. 2
⊢
((2↑;;100) mod 𝑁) = (;;614
mod 𝑁) |
| 364 | 11 | nn0cni 12538 |
. . 3
⊢ ;;100 ∈ ℂ |
| 365 | | eqid 2737 |
. . . 4
⊢ ;;100 = ;;100 |
| 366 | 20, 10, 3, 365, 173, 241 | decmul1 12797 |
. . 3
⊢ (;;100 · 2) = ;;200 |
| 367 | 364, 51, 366 | mulcomli 11270 |
. 2
⊢ (2
· ;;100) = ;;200 |
| 368 | | eqid 2737 |
. . . 4
⊢ ;;902 = ;;902 |
| 369 | | eqid 2737 |
. . . . . 6
⊢ ;90 = ;90 |
| 370 | 12, 3, 12, 369, 75 | decaddi 12793 |
. . . . 5
⊢ (;90 + 9) = ;99 |
| 371 | | eqid 2737 |
. . . . . . 7
⊢ ;94 = ;94 |
| 372 | | 6p1e7 12414 |
. . . . . . . 8
⊢ (6 + 1) =
7 |
| 373 | | 9t4e36 12857 |
. . . . . . . 8
⊢ (9
· 4) = ;36 |
| 374 | 41, 15, 372, 373 | decsuc 12764 |
. . . . . . 7
⊢ ((9
· 4) + 1) = ;37 |
| 375 | 103, 61 | oveq12i 7443 |
. . . . . . . 8
⊢ ((4
· 4) + (0 + 0)) = (;16 +
0) |
| 376 | 16, 15 | deccl 12748 |
. . . . . . . . . 10
⊢ ;16 ∈
ℕ0 |
| 377 | 376 | nn0cni 12538 |
. . . . . . . . 9
⊢ ;16 ∈ ℂ |
| 378 | 377 | addridi 11448 |
. . . . . . . 8
⊢ (;16 + 0) = ;16 |
| 379 | 375, 378 | eqtri 2765 |
. . . . . . 7
⊢ ((4
· 4) + (0 + 0)) = ;16 |
| 380 | 12, 2, 292, 371, 2, 15, 16, 374, 379 | decrmac 12791 |
. . . . . 6
⊢ ((;94 · 4) + (0 + 0)) = ;;376 |
| 381 | 238 | mul01i 11451 |
. . . . . . . 8
⊢ (;94 · 0) = 0 |
| 382 | 381 | oveq1i 7441 |
. . . . . . 7
⊢ ((;94 · 0) + 9) = (0 +
9) |
| 383 | 382, 75, 58 | 3eqtri 2769 |
. . . . . 6
⊢ ((;94 · 0) + 9) = ;09 |
| 384 | 2, 3, 3, 12, 60, 59, 13, 12, 3, 380, 383 | decma2c 12786 |
. . . . 5
⊢ ((;94 · ;40) + (9 + 0)) = ;;;3769 |
| 385 | 4, 3, 12, 12, 55, 370, 13, 12, 3, 384, 383 | decma2c 12786 |
. . . 4
⊢ ((;94 · ;;400) +
(;90 + 9)) = ;;;;37699 |
| 386 | 56 | mulridi 11265 |
. . . . 5
⊢ (9
· 1) = 9 |
| 387 | 64 | mulridi 11265 |
. . . . . . 7
⊢ (4
· 1) = 4 |
| 388 | 387 | oveq1i 7441 |
. . . . . 6
⊢ ((4
· 1) + 2) = (4 + 2) |
| 389 | 388, 203 | eqtri 2765 |
. . . . 5
⊢ ((4
· 1) + 2) = 6 |
| 390 | 12, 2, 20, 371, 16, 386, 389 | decrmanc 12790 |
. . . 4
⊢ ((;94 · 1) + 2) = ;96 |
| 391 | 5, 16, 19, 20, 1, 368, 13, 15, 12, 385, 390 | decma2c 12786 |
. . 3
⊢ ((;94 · 𝑁) + ;;902) =
;;;;;376996 |
| 392 | 38, 22 | deccl 12748 |
. . . 4
⊢ ;;245 ∈ ℕ0 |
| 393 | | eqid 2737 |
. . . . 5
⊢ ;;245 = ;;245 |
| 394 | 50, 51, 199 | addcomli 11453 |
. . . . . . 7
⊢ (2 + 6) =
8 |
| 395 | 20, 2, 15, 16, 165, 287, 394, 101 | decadd 12787 |
. . . . . 6
⊢ (;24 + ;61) = ;85 |
| 396 | | 8p2e10 12813 |
. . . . . . 7
⊢ (8 + 2) =
;10 |
| 397 | 41, 15, 372, 90 | decsuc 12764 |
. . . . . . 7
⊢ ((6
· 6) + 1) = ;37 |
| 398 | 50 | mullidi 11266 |
. . . . . . . . 9
⊢ (1
· 6) = 6 |
| 399 | 398 | oveq1i 7441 |
. . . . . . . 8
⊢ ((1
· 6) + 0) = (6 + 0) |
| 400 | 50 | addridi 11448 |
. . . . . . . 8
⊢ (6 + 0) =
6 |
| 401 | 399, 400 | eqtri 2765 |
. . . . . . 7
⊢ ((1
· 6) + 0) = 6 |
| 402 | 15, 16, 16, 3, 287, 396, 15, 397, 401 | decma 12784 |
. . . . . 6
⊢ ((;61 · 6) + (8 + 2)) = ;;376 |
| 403 | 17, 2, 24, 22, 285, 395, 15, 12, 20, 402, 99 | decmac 12785 |
. . . . 5
⊢ ((;;614 · 6) + (;24 + ;61)) = ;;;3769 |
| 404 | 16, 15, 16, 287, 317, 78 | decmul1 12797 |
. . . . . 6
⊢ (;61 · 1) = ;61 |
| 405 | 387 | oveq1i 7441 |
. . . . . . 7
⊢ ((4
· 1) + 5) = (4 + 5) |
| 406 | 405, 98 | eqtri 2765 |
. . . . . 6
⊢ ((4
· 1) + 5) = 9 |
| 407 | 17, 2, 22, 285, 16, 404, 406 | decrmanc 12790 |
. . . . 5
⊢ ((;;614 · 1) + 5) = ;;619 |
| 408 | 15, 16, 38, 22, 287, 393, 18, 12, 17, 403, 407 | decma2c 12786 |
. . . 4
⊢ ((;;614 · ;61) + ;;245) =
;;;;37699 |
| 409 | 65 | oveq1i 7441 |
. . . . . . 7
⊢ ((1
· 4) + 1) = (4 + 1) |
| 410 | 409, 101 | eqtri 2765 |
. . . . . 6
⊢ ((1
· 4) + 1) = 5 |
| 411 | 15, 16, 16, 287, 2, 95, 410 | decrmanc 12790 |
. . . . 5
⊢ ((;61 · 4) + 1) = ;;245 |
| 412 | 2, 17, 2, 285, 15, 16, 411, 103 | decmul1c 12798 |
. . . 4
⊢ (;;614 · 4) = ;;;2456 |
| 413 | 18, 17, 2, 285, 15, 392, 408, 412 | decmul2c 12799 |
. . 3
⊢ (;;614 · ;;614) =
;;;;;376996 |
| 414 | 391, 413 | eqtr4i 2768 |
. 2
⊢ ((;94 · 𝑁) + ;;902) =
(;;614 · ;;614) |
| 415 | 8, 9, 11, 14, 18, 21, 363, 367, 414 | mod2xi 17107 |
1
⊢
((2↑;;200) mod 𝑁) = (;;902
mod 𝑁) |