Proof of Theorem 4001lem2
| 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 |  | 9nn0 12550 | . . . . 5
⊢ 9 ∈
ℕ0 | 
| 11 | 2, 10 | deccl 12748 | . . . 4
⊢ ;49 ∈
ℕ0 | 
| 12 | 11, 3 | deccl 12748 | . . 3
⊢ ;;490 ∈ ℕ0 | 
| 13 | 12 | nn0zi 12642 | . 2
⊢ ;;490 ∈ ℤ | 
| 14 |  | 1nn0 12542 | . . . . 5
⊢ 1 ∈
ℕ0 | 
| 15 | 14, 2 | deccl 12748 | . . . 4
⊢ ;14 ∈
ℕ0 | 
| 16 | 15, 3 | deccl 12748 | . . 3
⊢ ;;140 ∈ ℕ0 | 
| 17 | 16, 14 | deccl 12748 | . 2
⊢ ;;;1401
∈ ℕ0 | 
| 18 |  | 2nn0 12543 | . . . . 5
⊢ 2 ∈
ℕ0 | 
| 19 |  | 3nn0 12544 | . . . . 5
⊢ 3 ∈
ℕ0 | 
| 20 | 18, 19 | deccl 12748 | . . . 4
⊢ ;23 ∈
ℕ0 | 
| 21 | 20, 14 | deccl 12748 | . . 3
⊢ ;;231 ∈ ℕ0 | 
| 22 | 21, 14 | deccl 12748 | . 2
⊢ ;;;2311
∈ ℕ0 | 
| 23 | 18, 3 | deccl 12748 | . . . 4
⊢ ;20 ∈
ℕ0 | 
| 24 | 23, 3 | deccl 12748 | . . 3
⊢ ;;200 ∈ ℕ0 | 
| 25 | 23, 19 | deccl 12748 | . . . 4
⊢ ;;203 ∈ ℕ0 | 
| 26 | 25 | nn0zi 12642 | . . 3
⊢ ;;203 ∈ ℤ | 
| 27 | 10, 3 | deccl 12748 | . . . 4
⊢ ;90 ∈
ℕ0 | 
| 28 | 27, 18 | deccl 12748 | . . 3
⊢ ;;902 ∈ ℕ0 | 
| 29 | 1 | 4001lem1 17178 | . . 3
⊢
((2↑;;200) mod 𝑁) = (;;902
mod 𝑁) | 
| 30 | 24 | nn0cni 12538 | . . . 4
⊢ ;;200 ∈ ℂ | 
| 31 |  | 2cn 12341 | . . . 4
⊢ 2 ∈
ℂ | 
| 32 |  | eqid 2737 | . . . . 5
⊢ ;;200 = ;;200 | 
| 33 |  | eqid 2737 | . . . . . 6
⊢ ;20 = ;20 | 
| 34 |  | 2t2e4 12430 | . . . . . 6
⊢ (2
· 2) = 4 | 
| 35 | 31 | mul02i 11450 | . . . . . 6
⊢ (0
· 2) = 0 | 
| 36 | 18, 18, 3, 33, 34, 35 | decmul1 12797 | . . . . 5
⊢ (;20 · 2) = ;40 | 
| 37 | 18, 23, 3, 32, 36, 35 | decmul1 12797 | . . . 4
⊢ (;;200 · 2) = ;;400 | 
| 38 | 30, 31, 37 | mulcomli 11270 | . . 3
⊢ (2
· ;;200) = ;;400 | 
| 39 |  | eqid 2737 | . . . . 5
⊢ ;;;1401 =
;;;1401 | 
| 40 |  | 6nn0 12547 | . . . . . . 7
⊢ 6 ∈
ℕ0 | 
| 41 | 14, 40 | deccl 12748 | . . . . . 6
⊢ ;16 ∈
ℕ0 | 
| 42 |  | eqid 2737 | . . . . . 6
⊢ ;;400 = ;;400 | 
| 43 |  | eqid 2737 | . . . . . . 7
⊢ ;;140 = ;;140 | 
| 44 |  | eqid 2737 | . . . . . . . 8
⊢ ;14 = ;14 | 
| 45 |  | 4p2e6 12419 | . . . . . . . 8
⊢ (4 + 2) =
6 | 
| 46 | 14, 2, 18, 44, 45 | decaddi 12793 | . . . . . . 7
⊢ (;14 + 2) = ;16 | 
| 47 |  | 00id 11436 | . . . . . . 7
⊢ (0 + 0) =
0 | 
| 48 | 15, 3, 18, 3, 43, 33, 46, 47 | decadd 12787 | . . . . . 6
⊢ (;;140 + ;20) = ;;160 | 
| 49 |  | eqid 2737 | . . . . . . 7
⊢ ;40 = ;40 | 
| 50 | 41 | nn0cni 12538 | . . . . . . . 8
⊢ ;16 ∈ ℂ | 
| 51 | 50 | addridi 11448 | . . . . . . 7
⊢ (;16 + 0) = ;16 | 
| 52 |  | eqid 2737 | . . . . . . . 8
⊢ ;;203 = ;;203 | 
| 53 |  | ax-1cn 11213 | . . . . . . . . . 10
⊢ 1 ∈
ℂ | 
| 54 | 53 | addridi 11448 | . . . . . . . . 9
⊢ (1 + 0) =
1 | 
| 55 | 14 | dec0h 12755 | . . . . . . . . 9
⊢ 1 = ;01 | 
| 56 | 54, 55 | eqtri 2765 | . . . . . . . 8
⊢ (1 + 0) =
;01 | 
| 57 | 53 | addlidi 11449 | . . . . . . . . . 10
⊢ (0 + 1) =
1 | 
| 58 | 57, 14 | eqeltri 2837 | . . . . . . . . 9
⊢ (0 + 1)
∈ ℕ0 | 
| 59 |  | 4cn 12351 | . . . . . . . . . 10
⊢ 4 ∈
ℂ | 
| 60 |  | 4t2e8 12434 | . . . . . . . . . 10
⊢ (4
· 2) = 8 | 
| 61 | 59, 31, 60 | mulcomli 11270 | . . . . . . . . 9
⊢ (2
· 4) = 8 | 
| 62 | 59 | mul02i 11450 | . . . . . . . . . . 11
⊢ (0
· 4) = 0 | 
| 63 | 62, 57 | oveq12i 7443 | . . . . . . . . . 10
⊢ ((0
· 4) + (0 + 1)) = (0 + 1) | 
| 64 | 63, 57 | eqtri 2765 | . . . . . . . . 9
⊢ ((0
· 4) + (0 + 1)) = 1 | 
| 65 | 18, 3, 58, 33, 2, 61, 64 | decrmanc 12790 | . . . . . . . 8
⊢ ((;20 · 4) + (0 + 1)) = ;81 | 
| 66 |  | 2p1e3 12408 | . . . . . . . . 9
⊢ (2 + 1) =
3 | 
| 67 |  | 3cn 12347 | . . . . . . . . . 10
⊢ 3 ∈
ℂ | 
| 68 |  | 4t3e12 12831 | . . . . . . . . . 10
⊢ (4
· 3) = ;12 | 
| 69 | 59, 67, 68 | mulcomli 11270 | . . . . . . . . 9
⊢ (3
· 4) = ;12 | 
| 70 | 14, 18, 66, 69 | decsuc 12764 | . . . . . . . 8
⊢ ((3
· 4) + 1) = ;13 | 
| 71 | 23, 19, 3, 14, 52, 56, 2, 19, 14, 65, 70 | decmac 12785 | . . . . . . 7
⊢ ((;;203 · 4) + (1 + 0)) = ;;813 | 
| 72 | 25 | nn0cni 12538 | . . . . . . . . . 10
⊢ ;;203 ∈ ℂ | 
| 73 | 72 | mul01i 11451 | . . . . . . . . 9
⊢ (;;203 · 0) = 0 | 
| 74 | 73 | oveq1i 7441 | . . . . . . . 8
⊢ ((;;203 · 0) + 6) = (0 + 6) | 
| 75 |  | 6cn 12357 | . . . . . . . . 9
⊢ 6 ∈
ℂ | 
| 76 | 75 | addlidi 11449 | . . . . . . . 8
⊢ (0 + 6) =
6 | 
| 77 | 40 | dec0h 12755 | . . . . . . . 8
⊢ 6 = ;06 | 
| 78 | 74, 76, 77 | 3eqtri 2769 | . . . . . . 7
⊢ ((;;203 · 0) + 6) = ;06 | 
| 79 | 2, 3, 14, 40, 49, 51, 25, 40, 3, 71, 78 | decma2c 12786 | . . . . . 6
⊢ ((;;203 · ;40) + (;16 + 0)) = ;;;8136 | 
| 80 | 73 | oveq1i 7441 | . . . . . . 7
⊢ ((;;203 · 0) + 0) = (0 + 0) | 
| 81 | 3 | dec0h 12755 | . . . . . . 7
⊢ 0 = ;00 | 
| 82 | 80, 47, 81 | 3eqtri 2769 | . . . . . 6
⊢ ((;;203 · 0) + 0) = ;00 | 
| 83 | 4, 3, 41, 3, 42, 48, 25, 3, 3, 79, 82 | decma2c 12786 | . . . . 5
⊢ ((;;203 · ;;400) +
(;;140 + ;20)) = ;;;;81360 | 
| 84 | 31 | mulridi 11265 | . . . . . . 7
⊢ (2
· 1) = 2 | 
| 85 | 53 | mul02i 11450 | . . . . . . 7
⊢ (0
· 1) = 0 | 
| 86 | 14, 18, 3, 33, 84, 85 | decmul1 12797 | . . . . . 6
⊢ (;20 · 1) = ;20 | 
| 87 | 67 | mulridi 11265 | . . . . . . . 8
⊢ (3
· 1) = 3 | 
| 88 | 87 | oveq1i 7441 | . . . . . . 7
⊢ ((3
· 1) + 1) = (3 + 1) | 
| 89 |  | 3p1e4 12411 | . . . . . . 7
⊢ (3 + 1) =
4 | 
| 90 | 88, 89 | eqtri 2765 | . . . . . 6
⊢ ((3
· 1) + 1) = 4 | 
| 91 | 23, 19, 14, 52, 14, 86, 90 | decrmanc 12790 | . . . . 5
⊢ ((;;203 · 1) + 1) = ;;204 | 
| 92 | 5, 14, 16, 14, 1, 39, 25, 2, 23, 83, 91 | decma2c 12786 | . . . 4
⊢ ((;;203 · 𝑁) + ;;;1401) = ;;;;;813604 | 
| 93 |  | eqid 2737 | . . . . 5
⊢ ;;902 = ;;902 | 
| 94 |  | 8nn0 12549 | . . . . . . 7
⊢ 8 ∈
ℕ0 | 
| 95 | 14, 94 | deccl 12748 | . . . . . 6
⊢ ;18 ∈
ℕ0 | 
| 96 | 95, 3 | deccl 12748 | . . . . 5
⊢ ;;180 ∈ ℕ0 | 
| 97 |  | eqid 2737 | . . . . . 6
⊢ ;90 = ;90 | 
| 98 |  | eqid 2737 | . . . . . 6
⊢ ;;180 = ;;180 | 
| 99 | 95 | nn0cni 12538 | . . . . . . . 8
⊢ ;18 ∈ ℂ | 
| 100 | 99 | addridi 11448 | . . . . . . 7
⊢ (;18 + 0) = ;18 | 
| 101 |  | 1p2e3 12409 | . . . . . . . . 9
⊢ (1 + 2) =
3 | 
| 102 | 101, 19 | eqeltri 2837 | . . . . . . . 8
⊢ (1 + 2)
∈ ℕ0 | 
| 103 |  | 9t9e81 12862 | . . . . . . . 8
⊢ (9
· 9) = ;81 | 
| 104 |  | 9cn 12366 | . . . . . . . . . . 11
⊢ 9 ∈
ℂ | 
| 105 | 104 | mul02i 11450 | . . . . . . . . . 10
⊢ (0
· 9) = 0 | 
| 106 | 105, 101 | oveq12i 7443 | . . . . . . . . 9
⊢ ((0
· 9) + (1 + 2)) = (0 + 3) | 
| 107 | 67 | addlidi 11449 | . . . . . . . . 9
⊢ (0 + 3) =
3 | 
| 108 | 106, 107 | eqtri 2765 | . . . . . . . 8
⊢ ((0
· 9) + (1 + 2)) = 3 | 
| 109 | 10, 3, 102, 97, 10, 103, 108 | decrmanc 12790 | . . . . . . 7
⊢ ((;90 · 9) + (1 + 2)) = ;;813 | 
| 110 |  | 9t2e18 12855 | . . . . . . . . 9
⊢ (9
· 2) = ;18 | 
| 111 | 104, 31, 110 | mulcomli 11270 | . . . . . . . 8
⊢ (2
· 9) = ;18 | 
| 112 |  | 1p1e2 12391 | . . . . . . . 8
⊢ (1 + 1) =
2 | 
| 113 |  | 8p8e16 12819 | . . . . . . . 8
⊢ (8 + 8) =
;16 | 
| 114 | 14, 94, 94, 111, 112, 40, 113 | decaddci 12794 | . . . . . . 7
⊢ ((2
· 9) + 8) = ;26 | 
| 115 | 27, 18, 14, 94, 93, 100, 10, 40, 18, 109, 114 | decmac 12785 | . . . . . 6
⊢ ((;;902 · 9) + (;18 + 0)) = ;;;8136 | 
| 116 | 28 | nn0cni 12538 | . . . . . . . . 9
⊢ ;;902 ∈ ℂ | 
| 117 | 116 | mul01i 11451 | . . . . . . . 8
⊢ (;;902 · 0) = 0 | 
| 118 | 117 | oveq1i 7441 | . . . . . . 7
⊢ ((;;902 · 0) + 0) = (0 + 0) | 
| 119 | 118, 47, 81 | 3eqtri 2769 | . . . . . 6
⊢ ((;;902 · 0) + 0) = ;00 | 
| 120 | 10, 3, 95, 3, 97, 98, 28, 3, 3, 115, 119 | decma2c 12786 | . . . . 5
⊢ ((;;902 · ;90) + ;;180) =
;;;;81360 | 
| 121 | 18, 10, 3, 97, 110, 35 | decmul1 12797 | . . . . . 6
⊢ (;90 · 2) = ;;180 | 
| 122 | 18, 27, 18, 93, 121, 34 | decmul1 12797 | . . . . 5
⊢ (;;902 · 2) = ;;;1804 | 
| 123 | 28, 27, 18, 93, 2, 96, 120, 122 | decmul2c 12799 | . . . 4
⊢ (;;902 · ;;902) =
;;;;;813604 | 
| 124 | 92, 123 | eqtr4i 2768 | . . 3
⊢ ((;;203 · 𝑁) + ;;;1401) = (;;902
· ;;902) | 
| 125 | 8, 9, 24, 26, 28, 17, 29, 38, 124 | mod2xi 17107 | . 2
⊢
((2↑;;400) mod 𝑁) = (;;;1401 mod 𝑁) | 
| 126 | 5 | nn0cni 12538 | . . 3
⊢ ;;400 ∈ ℂ | 
| 127 | 18, 2, 3, 49, 60, 35 | decmul1 12797 | . . . 4
⊢ (;40 · 2) = ;80 | 
| 128 | 18, 4, 3, 42, 127, 35 | decmul1 12797 | . . 3
⊢ (;;400 · 2) = ;;800 | 
| 129 | 126, 31, 128 | mulcomli 11270 | . 2
⊢ (2
· ;;400) = ;;800 | 
| 130 |  | eqid 2737 | . . . 4
⊢ ;;;2311 =
;;;2311 | 
| 131 | 18, 94 | deccl 12748 | . . . . 5
⊢ ;28 ∈
ℕ0 | 
| 132 |  | eqid 2737 | . . . . . 6
⊢ ;;231 = ;;231 | 
| 133 |  | eqid 2737 | . . . . . 6
⊢ ;49 = ;49 | 
| 134 |  | 7nn0 12548 | . . . . . . 7
⊢ 7 ∈
ℕ0 | 
| 135 |  | 7p1e8 12415 | . . . . . . 7
⊢ (7 + 1) =
8 | 
| 136 |  | eqid 2737 | . . . . . . . 8
⊢ ;23 = ;23 | 
| 137 |  | 4p3e7 12420 | . . . . . . . . 9
⊢ (4 + 3) =
7 | 
| 138 | 59, 67, 137 | addcomli 11453 | . . . . . . . 8
⊢ (3 + 4) =
7 | 
| 139 | 18, 19, 2, 136, 138 | decaddi 12793 | . . . . . . 7
⊢ (;23 + 4) = ;27 | 
| 140 | 18, 134, 135, 139 | decsuc 12764 | . . . . . 6
⊢ ((;23 + 4) + 1) = ;28 | 
| 141 |  | 9p1e10 12735 | . . . . . . 7
⊢ (9 + 1) =
;10 | 
| 142 | 104, 53, 141 | addcomli 11453 | . . . . . 6
⊢ (1 + 9) =
;10 | 
| 143 | 20, 14, 2, 10, 132, 133, 140, 142 | decaddc2 12789 | . . . . 5
⊢ (;;231 + ;49) = ;;280 | 
| 144 | 131 | nn0cni 12538 | . . . . . . 7
⊢ ;28 ∈ ℂ | 
| 145 | 144 | addridi 11448 | . . . . . 6
⊢ (;28 + 0) = ;28 | 
| 146 | 31 | addridi 11448 | . . . . . . . 8
⊢ (2 + 0) =
2 | 
| 147 | 146, 18 | eqeltri 2837 | . . . . . . 7
⊢ (2 + 0)
∈ ℕ0 | 
| 148 |  | eqid 2737 | . . . . . . 7
⊢ ;;490 = ;;490 | 
| 149 |  | 4t4e16 12832 | . . . . . . . . 9
⊢ (4
· 4) = ;16 | 
| 150 |  | 6p3e9 12426 | . . . . . . . . 9
⊢ (6 + 3) =
9 | 
| 151 | 14, 40, 19, 149, 150 | decaddi 12793 | . . . . . . . 8
⊢ ((4
· 4) + 3) = ;19 | 
| 152 |  | 9t4e36 12857 | . . . . . . . 8
⊢ (9
· 4) = ;36 | 
| 153 | 2, 2, 10, 133, 40, 19, 151, 152 | decmul1c 12798 | . . . . . . 7
⊢ (;49 · 4) = ;;196 | 
| 154 | 62, 146 | oveq12i 7443 | . . . . . . . 8
⊢ ((0
· 4) + (2 + 0)) = (0 + 2) | 
| 155 | 31 | addlidi 11449 | . . . . . . . 8
⊢ (0 + 2) =
2 | 
| 156 | 154, 155 | eqtri 2765 | . . . . . . 7
⊢ ((0
· 4) + (2 + 0)) = 2 | 
| 157 | 11, 3, 147, 148, 2, 153, 156 | decrmanc 12790 | . . . . . 6
⊢ ((;;490 · 4) + (2 + 0)) = ;;;1962 | 
| 158 | 12 | nn0cni 12538 | . . . . . . . . 9
⊢ ;;490 ∈ ℂ | 
| 159 | 158 | mul01i 11451 | . . . . . . . 8
⊢ (;;490 · 0) = 0 | 
| 160 | 159 | oveq1i 7441 | . . . . . . 7
⊢ ((;;490 · 0) + 8) = (0 + 8) | 
| 161 |  | 8cn 12363 | . . . . . . . 8
⊢ 8 ∈
ℂ | 
| 162 | 161 | addlidi 11449 | . . . . . . 7
⊢ (0 + 8) =
8 | 
| 163 | 94 | dec0h 12755 | . . . . . . 7
⊢ 8 = ;08 | 
| 164 | 160, 162,
163 | 3eqtri 2769 | . . . . . 6
⊢ ((;;490 · 0) + 8) = ;08 | 
| 165 | 2, 3, 18, 94, 49, 145, 12, 94, 3, 157, 164 | decma2c 12786 | . . . . 5
⊢ ((;;490 · ;40) + (;28 + 0)) = ;;;;19628 | 
| 166 | 159 | oveq1i 7441 | . . . . . 6
⊢ ((;;490 · 0) + 0) = (0 + 0) | 
| 167 | 166, 47, 81 | 3eqtri 2769 | . . . . 5
⊢ ((;;490 · 0) + 0) = ;00 | 
| 168 | 4, 3, 131, 3, 42, 143, 12, 3, 3, 165, 167 | decma2c 12786 | . . . 4
⊢ ((;;490 · ;;400) +
(;;231 + ;49)) = ;;;;;196280 | 
| 169 | 59 | mulridi 11265 | . . . . . 6
⊢ (4
· 1) = 4 | 
| 170 | 104 | mulridi 11265 | . . . . . 6
⊢ (9
· 1) = 9 | 
| 171 | 14, 2, 10, 133, 169, 170 | decmul1 12797 | . . . . 5
⊢ (;49 · 1) = ;49 | 
| 172 | 85 | oveq1i 7441 | . . . . . 6
⊢ ((0
· 1) + 1) = (0 + 1) | 
| 173 | 172, 57 | eqtri 2765 | . . . . 5
⊢ ((0
· 1) + 1) = 1 | 
| 174 | 11, 3, 14, 148, 14, 171, 173 | decrmanc 12790 | . . . 4
⊢ ((;;490 · 1) + 1) = ;;491 | 
| 175 | 5, 14, 21, 14, 1, 130, 12, 14, 11, 168, 174 | decma2c 12786 | . . 3
⊢ ((;;490 · 𝑁) + ;;;2311) = ;;;;;;1962801 | 
| 176 | 15 | nn0cni 12538 | . . . . . . 7
⊢ ;14 ∈ ℂ | 
| 177 | 176 | addridi 11448 | . . . . . 6
⊢ (;14 + 0) = ;14 | 
| 178 |  | 5nn0 12546 | . . . . . . . 8
⊢ 5 ∈
ℕ0 | 
| 179 | 178, 40 | deccl 12748 | . . . . . . 7
⊢ ;56 ∈
ℕ0 | 
| 180 | 179, 3 | deccl 12748 | . . . . . 6
⊢ ;;560 ∈ ℕ0 | 
| 181 |  | eqid 2737 | . . . . . . . 8
⊢ ;;560 = ;;560 | 
| 182 | 179 | nn0cni 12538 | . . . . . . . . 9
⊢ ;56 ∈ ℂ | 
| 183 | 182 | addlidi 11449 | . . . . . . . 8
⊢ (0 +
;56) = ;56 | 
| 184 | 3, 14, 179, 3, 55, 181, 183, 54 | decadd 12787 | . . . . . . 7
⊢ (1 +
;;560) = ;;561 | 
| 185 | 182 | addridi 11448 | . . . . . . . 8
⊢ (;56 + 0) = ;56 | 
| 186 |  | 5cn 12354 | . . . . . . . . . . 11
⊢ 5 ∈
ℂ | 
| 187 | 186 | addridi 11448 | . . . . . . . . . 10
⊢ (5 + 0) =
5 | 
| 188 | 187, 178 | eqeltri 2837 | . . . . . . . . 9
⊢ (5 + 0)
∈ ℕ0 | 
| 189 | 53 | mulridi 11265 | . . . . . . . . 9
⊢ (1
· 1) = 1 | 
| 190 | 169, 187 | oveq12i 7443 | . . . . . . . . . 10
⊢ ((4
· 1) + (5 + 0)) = (4 + 5) | 
| 191 |  | 5p4e9 12424 | . . . . . . . . . . 11
⊢ (5 + 4) =
9 | 
| 192 | 186, 59, 191 | addcomli 11453 | . . . . . . . . . 10
⊢ (4 + 5) =
9 | 
| 193 | 190, 192 | eqtri 2765 | . . . . . . . . 9
⊢ ((4
· 1) + (5 + 0)) = 9 | 
| 194 | 14, 2, 188, 44, 14, 189, 193 | decrmanc 12790 | . . . . . . . 8
⊢ ((;14 · 1) + (5 + 0)) = ;19 | 
| 195 | 85 | oveq1i 7441 | . . . . . . . . 9
⊢ ((0
· 1) + 6) = (0 + 6) | 
| 196 | 195, 76, 77 | 3eqtri 2769 | . . . . . . . 8
⊢ ((0
· 1) + 6) = ;06 | 
| 197 | 15, 3, 178, 40, 43, 185, 14, 40, 3, 194, 196 | decmac 12785 | . . . . . . 7
⊢ ((;;140 · 1) + (;56 + 0)) = ;;196 | 
| 198 | 189 | oveq1i 7441 | . . . . . . . 8
⊢ ((1
· 1) + 1) = (1 + 1) | 
| 199 | 18 | dec0h 12755 | . . . . . . . 8
⊢ 2 = ;02 | 
| 200 | 198, 112,
199 | 3eqtri 2769 | . . . . . . 7
⊢ ((1
· 1) + 1) = ;02 | 
| 201 | 16, 14, 179, 14, 39, 184, 14, 18, 3, 197, 200 | decmac 12785 | . . . . . 6
⊢ ((;;;1401
· 1) + (1 + ;;560)) = ;;;1962 | 
| 202 | 59 | mullidi 11266 | . . . . . . . . . . . 12
⊢ (1
· 4) = 4 | 
| 203 | 202 | oveq1i 7441 | . . . . . . . . . . 11
⊢ ((1
· 4) + 1) = (4 + 1) | 
| 204 |  | 4p1e5 12412 | . . . . . . . . . . 11
⊢ (4 + 1) =
5 | 
| 205 | 203, 204 | eqtri 2765 | . . . . . . . . . 10
⊢ ((1
· 4) + 1) = 5 | 
| 206 | 2, 14, 2, 44, 40, 14, 205, 149 | decmul1c 12798 | . . . . . . . . 9
⊢ (;14 · 4) = ;56 | 
| 207 | 75 | addridi 11448 | . . . . . . . . 9
⊢ (6 + 0) =
6 | 
| 208 | 178, 40, 3, 206, 207 | decaddi 12793 | . . . . . . . 8
⊢ ((;14 · 4) + 0) = ;56 | 
| 209 |  | 0cn 11253 | . . . . . . . . 9
⊢ 0 ∈
ℂ | 
| 210 | 59 | mul01i 11451 | . . . . . . . . . 10
⊢ (4
· 0) = 0 | 
| 211 | 210, 81 | eqtri 2765 | . . . . . . . . 9
⊢ (4
· 0) = ;00 | 
| 212 | 59, 209, 211 | mulcomli 11270 | . . . . . . . 8
⊢ (0
· 4) = ;00 | 
| 213 | 2, 15, 3, 43, 3, 3,
208, 212 | decmul1c 12798 | . . . . . . 7
⊢ (;;140 · 4) = ;;560 | 
| 214 | 202 | oveq1i 7441 | . . . . . . . 8
⊢ ((1
· 4) + 4) = (4 + 4) | 
| 215 |  | 4p4e8 12421 | . . . . . . . 8
⊢ (4 + 4) =
8 | 
| 216 | 214, 215 | eqtri 2765 | . . . . . . 7
⊢ ((1
· 4) + 4) = 8 | 
| 217 | 16, 14, 2, 39, 2, 213, 216 | decrmanc 12790 | . . . . . 6
⊢ ((;;;1401
· 4) + 4) = ;;;5608 | 
| 218 | 14, 2, 14, 2, 44, 177, 17, 94, 180, 201, 217 | decma2c 12786 | . . . . 5
⊢ ((;;;1401
· ;14) + (;14 + 0)) = ;;;;19628 | 
| 219 | 17 | nn0cni 12538 | . . . . . . . 8
⊢ ;;;1401
∈ ℂ | 
| 220 | 219 | mul01i 11451 | . . . . . . 7
⊢ (;;;1401
· 0) = 0 | 
| 221 | 220 | oveq1i 7441 | . . . . . 6
⊢ ((;;;1401
· 0) + 0) = (0 + 0) | 
| 222 | 221, 47, 81 | 3eqtri 2769 | . . . . 5
⊢ ((;;;1401
· 0) + 0) = ;00 | 
| 223 | 15, 3, 15, 3, 43, 43, 17, 3, 3, 218, 222 | decma2c 12786 | . . . 4
⊢ ((;;;1401
· ;;140) + ;;140) =
;;;;;196280 | 
| 224 | 219 | mulridi 11265 | . . . 4
⊢ (;;;1401
· 1) = ;;;1401 | 
| 225 | 17, 16, 14, 39, 14, 16, 223, 224 | decmul2c 12799 | . . 3
⊢ (;;;1401
· ;;;1401)
= ;;;;;;1962801 | 
| 226 | 175, 225 | eqtr4i 2768 | . 2
⊢ ((;;490 · 𝑁) + ;;;2311) = (;;;1401 · ;;;1401) | 
| 227 | 8, 9, 5, 13, 17, 22, 125, 129, 226 | mod2xi 17107 | 1
⊢
((2↑;;800) mod 𝑁) = (;;;2311 mod 𝑁) |