Proof of Theorem 2503lem1
| Step | Hyp | Ref
| Expression |
| 1 | | 2503prm.1 |
. . 3
⊢ 𝑁 = ;;;2503 |
| 2 | | 2nn0 12543 |
. . . . . 6
⊢ 2 ∈
ℕ0 |
| 3 | | 5nn0 12546 |
. . . . . 6
⊢ 5 ∈
ℕ0 |
| 4 | 2, 3 | deccl 12748 |
. . . . 5
⊢ ;25 ∈
ℕ0 |
| 5 | | 0nn0 12541 |
. . . . 5
⊢ 0 ∈
ℕ0 |
| 6 | 4, 5 | deccl 12748 |
. . . 4
⊢ ;;250 ∈ ℕ0 |
| 7 | | 3nn 12345 |
. . . 4
⊢ 3 ∈
ℕ |
| 8 | 6, 7 | decnncl 12753 |
. . 3
⊢ ;;;2503
∈ ℕ |
| 9 | 1, 8 | eqeltri 2837 |
. 2
⊢ 𝑁 ∈ ℕ |
| 10 | | 2nn 12339 |
. 2
⊢ 2 ∈
ℕ |
| 11 | | 9nn0 12550 |
. 2
⊢ 9 ∈
ℕ0 |
| 12 | | 10nn0 12751 |
. . . 4
⊢ ;10 ∈
ℕ0 |
| 13 | | 4nn0 12545 |
. . . 4
⊢ 4 ∈
ℕ0 |
| 14 | 12, 13 | deccl 12748 |
. . 3
⊢ ;;104 ∈ ℕ0 |
| 15 | 14 | nn0zi 12642 |
. 2
⊢ ;;104 ∈ ℤ |
| 16 | | 1nn0 12542 |
. . . 4
⊢ 1 ∈
ℕ0 |
| 17 | 3, 16 | deccl 12748 |
. . 3
⊢ ;51 ∈
ℕ0 |
| 18 | 17, 2 | deccl 12748 |
. 2
⊢ ;;512 ∈ ℕ0 |
| 19 | | 8nn0 12549 |
. . . . 5
⊢ 8 ∈
ℕ0 |
| 20 | 16, 19 | deccl 12748 |
. . . 4
⊢ ;18 ∈
ℕ0 |
| 21 | | 3nn0 12544 |
. . . 4
⊢ 3 ∈
ℕ0 |
| 22 | 20, 21 | deccl 12748 |
. . 3
⊢ ;;183 ∈ ℕ0 |
| 23 | 22, 2 | deccl 12748 |
. 2
⊢ ;;;1832
∈ ℕ0 |
| 24 | | 8p1e9 12416 |
. . . 4
⊢ (8 + 1) =
9 |
| 25 | | 6nn0 12547 |
. . . . 5
⊢ 6 ∈
ℕ0 |
| 26 | | 2exp8 17126 |
. . . . 5
⊢
(2↑8) = ;;256 |
| 27 | | eqid 2737 |
. . . . . 6
⊢ ;25 = ;25 |
| 28 | 16 | dec0h 12755 |
. . . . . 6
⊢ 1 = ;01 |
| 29 | | 2t2e4 12430 |
. . . . . . . 8
⊢ (2
· 2) = 4 |
| 30 | | ax-1cn 11213 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
| 31 | 30 | addlidi 11449 |
. . . . . . . 8
⊢ (0 + 1) =
1 |
| 32 | 29, 31 | oveq12i 7443 |
. . . . . . 7
⊢ ((2
· 2) + (0 + 1)) = (4 + 1) |
| 33 | | 4p1e5 12412 |
. . . . . . 7
⊢ (4 + 1) =
5 |
| 34 | 32, 33 | eqtri 2765 |
. . . . . 6
⊢ ((2
· 2) + (0 + 1)) = 5 |
| 35 | | 5t2e10 12833 |
. . . . . . 7
⊢ (5
· 2) = ;10 |
| 36 | 16, 5, 31, 35 | decsuc 12764 |
. . . . . 6
⊢ ((5
· 2) + 1) = ;11 |
| 37 | 2, 3, 5, 16, 27, 28, 2, 16, 16, 34, 36 | decmac 12785 |
. . . . 5
⊢ ((;25 · 2) + 1) = ;51 |
| 38 | | 6t2e12 12837 |
. . . . 5
⊢ (6
· 2) = ;12 |
| 39 | 2, 4, 25, 26, 2, 16, 37, 38 | decmul1c 12798 |
. . . 4
⊢
((2↑8) · 2) = ;;512 |
| 40 | 2, 19, 24, 39 | numexpp1 17115 |
. . 3
⊢
(2↑9) = ;;512 |
| 41 | 40 | oveq1i 7441 |
. 2
⊢
((2↑9) mod 𝑁) =
(;;512 mod 𝑁) |
| 42 | | 9cn 12366 |
. . 3
⊢ 9 ∈
ℂ |
| 43 | | 2cn 12341 |
. . 3
⊢ 2 ∈
ℂ |
| 44 | | 9t2e18 12855 |
. . 3
⊢ (9
· 2) = ;18 |
| 45 | 42, 43, 44 | mulcomli 11270 |
. 2
⊢ (2
· 9) = ;18 |
| 46 | | eqid 2737 |
. . . 4
⊢ ;;;1832 =
;;;1832 |
| 47 | 21, 16 | deccl 12748 |
. . . 4
⊢ ;31 ∈
ℕ0 |
| 48 | 2, 16 | deccl 12748 |
. . . . 5
⊢ ;21 ∈
ℕ0 |
| 49 | | eqid 2737 |
. . . . 5
⊢ ;;250 = ;;250 |
| 50 | | eqid 2737 |
. . . . . 6
⊢ ;;183 = ;;183 |
| 51 | | eqid 2737 |
. . . . . 6
⊢ ;31 = ;31 |
| 52 | | eqid 2737 |
. . . . . . 7
⊢ ;18 = ;18 |
| 53 | | 1p1e2 12391 |
. . . . . . 7
⊢ (1 + 1) =
2 |
| 54 | | 8p3e11 12814 |
. . . . . . 7
⊢ (8 + 3) =
;11 |
| 55 | 16, 19, 21, 52, 53, 16, 54 | decaddci 12794 |
. . . . . 6
⊢ (;18 + 3) = ;21 |
| 56 | | 3p1e4 12411 |
. . . . . 6
⊢ (3 + 1) =
4 |
| 57 | 20, 21, 21, 16, 50, 51, 55, 56 | decadd 12787 |
. . . . 5
⊢ (;;183 + ;31) = ;;214 |
| 58 | 48 | nn0cni 12538 |
. . . . . . 7
⊢ ;21 ∈ ℂ |
| 59 | 58 | addridi 11448 |
. . . . . 6
⊢ (;21 + 0) = ;21 |
| 60 | 3, 2 | deccl 12748 |
. . . . . 6
⊢ ;52 ∈
ℕ0 |
| 61 | | eqid 2737 |
. . . . . . 7
⊢ ;;104 = ;;104 |
| 62 | 60 | nn0cni 12538 |
. . . . . . . 8
⊢ ;52 ∈ ℂ |
| 63 | | eqid 2737 |
. . . . . . . . 9
⊢ ;52 = ;52 |
| 64 | | 2p2e4 12401 |
. . . . . . . . 9
⊢ (2 + 2) =
4 |
| 65 | 3, 2, 2, 63, 64 | decaddi 12793 |
. . . . . . . 8
⊢ (;52 + 2) = ;54 |
| 66 | 62, 43, 65 | addcomli 11453 |
. . . . . . 7
⊢ (2 +
;52) = ;54 |
| 67 | 2 | dec0u 12754 |
. . . . . . . . 9
⊢ (;10 · 2) = ;20 |
| 68 | | 5p1e6 12413 |
. . . . . . . . 9
⊢ (5 + 1) =
6 |
| 69 | 67, 68 | oveq12i 7443 |
. . . . . . . 8
⊢ ((;10 · 2) + (5 + 1)) = (;20 + 6) |
| 70 | | eqid 2737 |
. . . . . . . . 9
⊢ ;20 = ;20 |
| 71 | | 6cn 12357 |
. . . . . . . . . 10
⊢ 6 ∈
ℂ |
| 72 | 71 | addlidi 11449 |
. . . . . . . . 9
⊢ (0 + 6) =
6 |
| 73 | 2, 5, 25, 70, 72 | decaddi 12793 |
. . . . . . . 8
⊢ (;20 + 6) = ;26 |
| 74 | 69, 73 | eqtri 2765 |
. . . . . . 7
⊢ ((;10 · 2) + (5 + 1)) = ;26 |
| 75 | | 4t2e8 12434 |
. . . . . . . . 9
⊢ (4
· 2) = 8 |
| 76 | 75 | oveq1i 7441 |
. . . . . . . 8
⊢ ((4
· 2) + 4) = (8 + 4) |
| 77 | | 8p4e12 12815 |
. . . . . . . 8
⊢ (8 + 4) =
;12 |
| 78 | 76, 77 | eqtri 2765 |
. . . . . . 7
⊢ ((4
· 2) + 4) = ;12 |
| 79 | 12, 13, 3, 13, 61, 66, 2, 2, 16, 74, 78 | decmac 12785 |
. . . . . 6
⊢ ((;;104 · 2) + (2 + ;52)) = ;;262 |
| 80 | 3 | dec0u 12754 |
. . . . . . . . 9
⊢ (;10 · 5) = ;50 |
| 81 | 43 | addlidi 11449 |
. . . . . . . . 9
⊢ (0 + 2) =
2 |
| 82 | 80, 81 | oveq12i 7443 |
. . . . . . . 8
⊢ ((;10 · 5) + (0 + 2)) = (;50 + 2) |
| 83 | | eqid 2737 |
. . . . . . . . 9
⊢ ;50 = ;50 |
| 84 | 3, 5, 2, 83, 81 | decaddi 12793 |
. . . . . . . 8
⊢ (;50 + 2) = ;52 |
| 85 | 82, 84 | eqtri 2765 |
. . . . . . 7
⊢ ((;10 · 5) + (0 + 2)) = ;52 |
| 86 | | 5cn 12354 |
. . . . . . . . 9
⊢ 5 ∈
ℂ |
| 87 | | 4cn 12351 |
. . . . . . . . 9
⊢ 4 ∈
ℂ |
| 88 | | 5t4e20 12835 |
. . . . . . . . 9
⊢ (5
· 4) = ;20 |
| 89 | 86, 87, 88 | mulcomli 11270 |
. . . . . . . 8
⊢ (4
· 5) = ;20 |
| 90 | 2, 5, 31, 89 | decsuc 12764 |
. . . . . . 7
⊢ ((4
· 5) + 1) = ;21 |
| 91 | 12, 13, 5, 16, 61, 28, 3, 16, 2, 85, 90 | decmac 12785 |
. . . . . 6
⊢ ((;;104 · 5) + 1) = ;;521 |
| 92 | 2, 3, 2, 16, 27, 59, 14, 16, 60, 79, 91 | decma2c 12786 |
. . . . 5
⊢ ((;;104 · ;25) + (;21 + 0)) = ;;;2621 |
| 93 | 14 | nn0cni 12538 |
. . . . . . . 8
⊢ ;;104 ∈ ℂ |
| 94 | 93 | mul01i 11451 |
. . . . . . 7
⊢ (;;104 · 0) = 0 |
| 95 | 94 | oveq1i 7441 |
. . . . . 6
⊢ ((;;104 · 0) + 4) = (0 + 4) |
| 96 | 87 | addlidi 11449 |
. . . . . 6
⊢ (0 + 4) =
4 |
| 97 | 13 | dec0h 12755 |
. . . . . 6
⊢ 4 = ;04 |
| 98 | 95, 96, 97 | 3eqtri 2769 |
. . . . 5
⊢ ((;;104 · 0) + 4) = ;04 |
| 99 | 4, 5, 48, 13, 49, 57, 14, 13, 5, 92, 98 | decma2c 12786 |
. . . 4
⊢ ((;;104 · ;;250) +
(;;183 + ;31)) = ;;;;26214 |
| 100 | | eqid 2737 |
. . . . . 6
⊢ ;10 = ;10 |
| 101 | | 3cn 12347 |
. . . . . . . . 9
⊢ 3 ∈
ℂ |
| 102 | 101 | mullidi 11266 |
. . . . . . . 8
⊢ (1
· 3) = 3 |
| 103 | | 00id 11436 |
. . . . . . . 8
⊢ (0 + 0) =
0 |
| 104 | 102, 103 | oveq12i 7443 |
. . . . . . 7
⊢ ((1
· 3) + (0 + 0)) = (3 + 0) |
| 105 | 101 | addridi 11448 |
. . . . . . 7
⊢ (3 + 0) =
3 |
| 106 | 104, 105 | eqtri 2765 |
. . . . . 6
⊢ ((1
· 3) + (0 + 0)) = 3 |
| 107 | 101 | mul02i 11450 |
. . . . . . . 8
⊢ (0
· 3) = 0 |
| 108 | 107 | oveq1i 7441 |
. . . . . . 7
⊢ ((0
· 3) + 1) = (0 + 1) |
| 109 | 108, 31, 28 | 3eqtri 2769 |
. . . . . 6
⊢ ((0
· 3) + 1) = ;01 |
| 110 | 16, 5, 5, 16, 100, 28, 21, 16, 5, 106, 109 | decmac 12785 |
. . . . 5
⊢ ((;10 · 3) + 1) = ;31 |
| 111 | | 4t3e12 12831 |
. . . . . 6
⊢ (4
· 3) = ;12 |
| 112 | 16, 2, 2, 111, 64 | decaddi 12793 |
. . . . 5
⊢ ((4
· 3) + 2) = ;14 |
| 113 | 12, 13, 2, 61, 21, 13, 16, 110, 112 | decrmac 12791 |
. . . 4
⊢ ((;;104 · 3) + 2) = ;;314 |
| 114 | 6, 21, 22, 2, 1, 46, 14, 13, 47, 99, 113 | decma2c 12786 |
. . 3
⊢ ((;;104 · 𝑁) + ;;;1832) = ;;;;;262144 |
| 115 | | eqid 2737 |
. . . 4
⊢ ;;512 = ;;512 |
| 116 | 12, 2 | deccl 12748 |
. . . 4
⊢ ;;102 ∈ ℕ0 |
| 117 | | eqid 2737 |
. . . . 5
⊢ ;51 = ;51 |
| 118 | | eqid 2737 |
. . . . 5
⊢ ;;102 = ;;102 |
| 119 | 86, 30, 68 | addcomli 11453 |
. . . . . . 7
⊢ (1 + 5) =
6 |
| 120 | 16, 5, 3, 16, 100, 117, 119, 31 | decadd 12787 |
. . . . . 6
⊢ (;10 + ;51) = ;61 |
| 121 | | 7nn0 12548 |
. . . . . . 7
⊢ 7 ∈
ℕ0 |
| 122 | | 6p1e7 12414 |
. . . . . . . 8
⊢ (6 + 1) =
7 |
| 123 | 121 | dec0h 12755 |
. . . . . . . 8
⊢ 7 = ;07 |
| 124 | 122, 123 | eqtri 2765 |
. . . . . . 7
⊢ (6 + 1) =
;07 |
| 125 | 31 | oveq2i 7442 |
. . . . . . . 8
⊢ ((5
· 5) + (0 + 1)) = ((5 · 5) + 1) |
| 126 | | 5t5e25 12836 |
. . . . . . . . 9
⊢ (5
· 5) = ;25 |
| 127 | 2, 3, 68, 126 | decsuc 12764 |
. . . . . . . 8
⊢ ((5
· 5) + 1) = ;26 |
| 128 | 125, 127 | eqtri 2765 |
. . . . . . 7
⊢ ((5
· 5) + (0 + 1)) = ;26 |
| 129 | 86 | mullidi 11266 |
. . . . . . . . 9
⊢ (1
· 5) = 5 |
| 130 | 129 | oveq1i 7441 |
. . . . . . . 8
⊢ ((1
· 5) + 7) = (5 + 7) |
| 131 | | 7cn 12360 |
. . . . . . . . 9
⊢ 7 ∈
ℂ |
| 132 | | 7p5e12 12810 |
. . . . . . . . 9
⊢ (7 + 5) =
;12 |
| 133 | 131, 86, 132 | addcomli 11453 |
. . . . . . . 8
⊢ (5 + 7) =
;12 |
| 134 | 130, 133 | eqtri 2765 |
. . . . . . 7
⊢ ((1
· 5) + 7) = ;12 |
| 135 | 3, 16, 5, 121, 117, 124, 3, 2, 16, 128, 134 | decmac 12785 |
. . . . . 6
⊢ ((;51 · 5) + (6 + 1)) = ;;262 |
| 136 | 86, 43, 35 | mulcomli 11270 |
. . . . . . 7
⊢ (2
· 5) = ;10 |
| 137 | 16, 5, 31, 136 | decsuc 12764 |
. . . . . 6
⊢ ((2
· 5) + 1) = ;11 |
| 138 | 17, 2, 25, 16, 115, 120, 3, 16, 16, 135, 137 | decmac 12785 |
. . . . 5
⊢ ((;;512 · 5) + (;10 + ;51)) = ;;;2621 |
| 139 | 17 | nn0cni 12538 |
. . . . . . 7
⊢ ;51 ∈ ℂ |
| 140 | 139 | mulridi 11265 |
. . . . . 6
⊢ (;51 · 1) = ;51 |
| 141 | 43 | mulridi 11265 |
. . . . . . . 8
⊢ (2
· 1) = 2 |
| 142 | 141 | oveq1i 7441 |
. . . . . . 7
⊢ ((2
· 1) + 2) = (2 + 2) |
| 143 | 142, 64 | eqtri 2765 |
. . . . . 6
⊢ ((2
· 1) + 2) = 4 |
| 144 | 17, 2, 2, 115, 16, 140, 143 | decrmanc 12790 |
. . . . 5
⊢ ((;;512 · 1) + 2) = ;;514 |
| 145 | 3, 16, 12, 2, 117, 118, 18, 13, 17, 138, 144 | decma2c 12786 |
. . . 4
⊢ ((;;512 · ;51) + ;;102) =
;;;;26214 |
| 146 | 43 | mullidi 11266 |
. . . . . 6
⊢ (1
· 2) = 2 |
| 147 | 2, 3, 16, 117, 35, 146 | decmul1 12797 |
. . . . 5
⊢ (;51 · 2) = ;;102 |
| 148 | 2, 17, 2, 115, 147, 29 | decmul1 12797 |
. . . 4
⊢ (;;512 · 2) = ;;;1024 |
| 149 | 18, 17, 2, 115, 13, 116, 145, 148 | decmul2c 12799 |
. . 3
⊢ (;;512 · ;;512) =
;;;;;262144 |
| 150 | 114, 149 | eqtr4i 2768 |
. 2
⊢ ((;;104 · 𝑁) + ;;;1832) = (;;512
· ;;512) |
| 151 | 9, 10, 11, 15, 18, 23, 41, 45, 150 | mod2xi 17107 |
1
⊢
((2↑;18) mod 𝑁) = (;;;1832 mod 𝑁) |