Proof of Theorem 2exp340mod341
| Step | Hyp | Ref
| Expression |
| 1 | | 3nn0 12544 |
. . . . 5
⊢ 3 ∈
ℕ0 |
| 2 | | 4nn0 12545 |
. . . . 5
⊢ 4 ∈
ℕ0 |
| 3 | 1, 2 | deccl 12748 |
. . . 4
⊢ ;34 ∈
ℕ0 |
| 4 | | 1nn 12277 |
. . . 4
⊢ 1 ∈
ℕ |
| 5 | 3, 4 | decnncl 12753 |
. . 3
⊢ ;;341 ∈ ℕ |
| 6 | | 2nn 12339 |
. . 3
⊢ 2 ∈
ℕ |
| 7 | | 1nn0 12542 |
. . . . 5
⊢ 1 ∈
ℕ0 |
| 8 | | 7nn0 12548 |
. . . . 5
⊢ 7 ∈
ℕ0 |
| 9 | 7, 8 | deccl 12748 |
. . . 4
⊢ ;17 ∈
ℕ0 |
| 10 | | 0nn0 12541 |
. . . 4
⊢ 0 ∈
ℕ0 |
| 11 | 9, 10 | deccl 12748 |
. . 3
⊢ ;;170 ∈ ℕ0 |
| 12 | | 0z 12624 |
. . 3
⊢ 0 ∈
ℤ |
| 13 | | 8nn0 12549 |
. . . . 5
⊢ 8 ∈
ℕ0 |
| 14 | | 5nn0 12546 |
. . . . 5
⊢ 5 ∈
ℕ0 |
| 15 | 13, 14 | deccl 12748 |
. . . 4
⊢ ;85 ∈
ℕ0 |
| 16 | | 3z 12650 |
. . . 4
⊢ 3 ∈
ℤ |
| 17 | | 2nn0 12543 |
. . . . 5
⊢ 2 ∈
ℕ0 |
| 18 | 1, 17 | deccl 12748 |
. . . 4
⊢ ;32 ∈
ℕ0 |
| 19 | 13, 2 | deccl 12748 |
. . . . 5
⊢ ;84 ∈
ℕ0 |
| 20 | | 6nn0 12547 |
. . . . . 6
⊢ 6 ∈
ℕ0 |
| 21 | 7, 20 | deccl 12748 |
. . . . 5
⊢ ;16 ∈
ℕ0 |
| 22 | 2, 17 | deccl 12748 |
. . . . . 6
⊢ ;42 ∈
ℕ0 |
| 23 | 17, 7 | deccl 12748 |
. . . . . . 7
⊢ ;21 ∈
ℕ0 |
| 24 | 17, 10 | deccl 12748 |
. . . . . . . 8
⊢ ;20 ∈
ℕ0 |
| 25 | 7, 10 | deccl 12748 |
. . . . . . . . 9
⊢ ;10 ∈
ℕ0 |
| 26 | | 2exp5 17123 |
. . . . . . . . . . 11
⊢
(2↑5) = ;32 |
| 27 | 26 | oveq1i 7441 |
. . . . . . . . . 10
⊢
((2↑5) mod ;;341) = (;32 mod ;;341) |
| 28 | | 5cn 12354 |
. . . . . . . . . . 11
⊢ 5 ∈
ℂ |
| 29 | | 2cn 12341 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
| 30 | | 5t2e10 12833 |
. . . . . . . . . . 11
⊢ (5
· 2) = ;10 |
| 31 | 28, 29, 30 | mulcomli 11270 |
. . . . . . . . . 10
⊢ (2
· 5) = ;10 |
| 32 | 25, 17 | deccl 12748 |
. . . . . . . . . . . 12
⊢ ;;102 ∈ ℕ0 |
| 33 | | 3p1e4 12411 |
. . . . . . . . . . . 12
⊢ (3 + 1) =
4 |
| 34 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ ;;;1023 =
;;;1023 |
| 35 | 32, 1, 33, 34 | decsuc 12764 |
. . . . . . . . . . 11
⊢ (;;;1023 +
1) = ;;;1024 |
| 36 | 1, 3, 7 | decmulnc 12800 |
. . . . . . . . . . . . 13
⊢ (3
· ;;341) = ;(3 · ;34)(3 · 1) |
| 37 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ ;34 = ;34 |
| 38 | | 3t3e9 12433 |
. . . . . . . . . . . . . . . . 17
⊢ (3
· 3) = 9 |
| 39 | 38 | oveq1i 7441 |
. . . . . . . . . . . . . . . 16
⊢ ((3
· 3) + 1) = (9 + 1) |
| 40 | | 9p1e10 12735 |
. . . . . . . . . . . . . . . 16
⊢ (9 + 1) =
;10 |
| 41 | 39, 40 | eqtri 2765 |
. . . . . . . . . . . . . . 15
⊢ ((3
· 3) + 1) = ;10 |
| 42 | | 4cn 12351 |
. . . . . . . . . . . . . . . 16
⊢ 4 ∈
ℂ |
| 43 | | 3cn 12347 |
. . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℂ |
| 44 | | 4t3e12 12831 |
. . . . . . . . . . . . . . . 16
⊢ (4
· 3) = ;12 |
| 45 | 42, 43, 44 | mulcomli 11270 |
. . . . . . . . . . . . . . 15
⊢ (3
· 4) = ;12 |
| 46 | 1, 1, 2, 37, 17, 7, 41, 45 | decmul2c 12799 |
. . . . . . . . . . . . . 14
⊢ (3
· ;34) = ;;102 |
| 47 | 43 | mulridi 11265 |
. . . . . . . . . . . . . 14
⊢ (3
· 1) = 3 |
| 48 | 46, 47 | deceq12i 12742 |
. . . . . . . . . . . . 13
⊢ ;(3 · ;34)(3 · 1) = ;;;1023 |
| 49 | 36, 48 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ (3
· ;;341) = ;;;1023 |
| 50 | 49 | oveq1i 7441 |
. . . . . . . . . . 11
⊢ ((3
· ;;341) + 1) = (;;;1023 + 1) |
| 51 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ ;32 = ;32 |
| 52 | 1, 1, 17 | decmulnc 12800 |
. . . . . . . . . . . . . 14
⊢ (3
· ;32) = ;(3 · 3)(3 · 2) |
| 53 | 52 | oveq1i 7441 |
. . . . . . . . . . . . 13
⊢ ((3
· ;32) + 6) = (;(3 · 3)(3 · 2) +
6) |
| 54 | | 9nn0 12550 |
. . . . . . . . . . . . . 14
⊢ 9 ∈
ℕ0 |
| 55 | | 3t2e6 12432 |
. . . . . . . . . . . . . . 15
⊢ (3
· 2) = 6 |
| 56 | 38, 55 | deceq12i 12742 |
. . . . . . . . . . . . . 14
⊢ ;(3 · 3)(3 · 2) = ;96 |
| 57 | | 6p6e12 12807 |
. . . . . . . . . . . . . 14
⊢ (6 + 6) =
;12 |
| 58 | 54, 20, 20, 56, 40, 17, 57 | decaddci 12794 |
. . . . . . . . . . . . 13
⊢ (;(3 · 3)(3 · 2) + 6) =
;;102 |
| 59 | 53, 58 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ ((3
· ;32) + 6) = ;;102 |
| 60 | 17, 1, 17 | decmulnc 12800 |
. . . . . . . . . . . . 13
⊢ (2
· ;32) = ;(2 · 3)(2 · 2) |
| 61 | 43, 29, 55 | mulcomli 11270 |
. . . . . . . . . . . . . 14
⊢ (2
· 3) = 6 |
| 62 | | 2t2e4 12430 |
. . . . . . . . . . . . . 14
⊢ (2
· 2) = 4 |
| 63 | 61, 62 | deceq12i 12742 |
. . . . . . . . . . . . 13
⊢ ;(2 · 3)(2 · 2) = ;64 |
| 64 | 60, 63 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ (2
· ;32) = ;64 |
| 65 | 18, 1, 17, 51, 2, 20, 59, 64 | decmul1c 12798 |
. . . . . . . . . . 11
⊢ (;32 · ;32) = ;;;1024 |
| 66 | 35, 50, 65 | 3eqtr4i 2775 |
. . . . . . . . . 10
⊢ ((3
· ;;341) + 1) = (;32 · ;32) |
| 67 | 5, 6, 14, 16, 18, 7, 27, 31, 66 | mod2xi 17107 |
. . . . . . . . 9
⊢
((2↑;10) mod ;;341) = (1 mod ;;341) |
| 68 | 17, 7, 10 | decmulnc 12800 |
. . . . . . . . . 10
⊢ (2
· ;10) = ;(2 · 1)(2 · 0) |
| 69 | 29 | mulridi 11265 |
. . . . . . . . . . 11
⊢ (2
· 1) = 2 |
| 70 | | 2t0e0 12435 |
. . . . . . . . . . 11
⊢ (2
· 0) = 0 |
| 71 | 69, 70 | deceq12i 12742 |
. . . . . . . . . 10
⊢ ;(2 · 1)(2 · 0) = ;20 |
| 72 | 68, 71 | eqtri 2765 |
. . . . . . . . 9
⊢ (2
· ;10) = ;20 |
| 73 | | 0p1e1 12388 |
. . . . . . . . . 10
⊢ (0 + 1) =
1 |
| 74 | 5 | nncni 12276 |
. . . . . . . . . . . 12
⊢ ;;341 ∈ ℂ |
| 75 | 74 | mul02i 11450 |
. . . . . . . . . . 11
⊢ (0
· ;;341) = 0 |
| 76 | 75 | oveq1i 7441 |
. . . . . . . . . 10
⊢ ((0
· ;;341) + 1) = (0 + 1) |
| 77 | | 1t1e1 12428 |
. . . . . . . . . 10
⊢ (1
· 1) = 1 |
| 78 | 73, 76, 77 | 3eqtr4i 2775 |
. . . . . . . . 9
⊢ ((0
· ;;341) + 1) = (1 · 1) |
| 79 | 5, 6, 25, 12, 7, 7, 67, 72, 78 | mod2xi 17107 |
. . . . . . . 8
⊢
((2↑;20) mod ;;341) = (1 mod ;;341) |
| 80 | | eqid 2737 |
. . . . . . . . 9
⊢ ;20 = ;20 |
| 81 | 17, 10, 73, 80 | decsuc 12764 |
. . . . . . . 8
⊢ (;20 + 1) = ;21 |
| 82 | 29 | addlidi 11449 |
. . . . . . . . 9
⊢ (0 + 2) =
2 |
| 83 | 75 | oveq1i 7441 |
. . . . . . . . 9
⊢ ((0
· ;;341) + 2) = (0 + 2) |
| 84 | 29 | mullidi 11266 |
. . . . . . . . 9
⊢ (1
· 2) = 2 |
| 85 | 82, 83, 84 | 3eqtr4i 2775 |
. . . . . . . 8
⊢ ((0
· ;;341) + 2) = (1 · 2) |
| 86 | 5, 6, 24, 12, 7, 17, 79, 81, 85 | modxp1i 17108 |
. . . . . . 7
⊢
((2↑;21) mod ;;341) = (2 mod ;;341) |
| 87 | 17, 17, 7 | decmulnc 12800 |
. . . . . . . 8
⊢ (2
· ;21) = ;(2 · 2)(2 · 1) |
| 88 | 62, 69 | deceq12i 12742 |
. . . . . . . 8
⊢ ;(2 · 2)(2 · 1) = ;42 |
| 89 | 87, 88 | eqtri 2765 |
. . . . . . 7
⊢ (2
· ;21) = ;42 |
| 90 | 42 | addlidi 11449 |
. . . . . . . 8
⊢ (0 + 4) =
4 |
| 91 | 75 | oveq1i 7441 |
. . . . . . . 8
⊢ ((0
· ;;341) + 4) = (0 + 4) |
| 92 | 90, 91, 62 | 3eqtr4i 2775 |
. . . . . . 7
⊢ ((0
· ;;341) + 4) = (2 · 2) |
| 93 | 5, 6, 23, 12, 17, 2, 86, 89, 92 | mod2xi 17107 |
. . . . . 6
⊢
((2↑;42) mod ;;341) = (4 mod ;;341) |
| 94 | 17, 2, 17 | decmulnc 12800 |
. . . . . . 7
⊢ (2
· ;42) = ;(2 · 4)(2 · 2) |
| 95 | | 4t2e8 12434 |
. . . . . . . . 9
⊢ (4
· 2) = 8 |
| 96 | 42, 29, 95 | mulcomli 11270 |
. . . . . . . 8
⊢ (2
· 4) = 8 |
| 97 | 96, 62 | deceq12i 12742 |
. . . . . . 7
⊢ ;(2 · 4)(2 · 2) = ;84 |
| 98 | 94, 97 | eqtri 2765 |
. . . . . 6
⊢ (2
· ;42) = ;84 |
| 99 | 21 | nn0cni 12538 |
. . . . . . . 8
⊢ ;16 ∈ ℂ |
| 100 | 99 | addlidi 11449 |
. . . . . . 7
⊢ (0 +
;16) = ;16 |
| 101 | 75 | oveq1i 7441 |
. . . . . . 7
⊢ ((0
· ;;341) + ;16) = (0 + ;16) |
| 102 | | 4t4e16 12832 |
. . . . . . 7
⊢ (4
· 4) = ;16 |
| 103 | 100, 101,
102 | 3eqtr4i 2775 |
. . . . . 6
⊢ ((0
· ;;341) + ;16) = (4 · 4) |
| 104 | 5, 6, 22, 12, 2, 21, 93, 98, 103 | mod2xi 17107 |
. . . . 5
⊢
((2↑;84) mod ;;341) = (;16 mod ;;341) |
| 105 | | 4p1e5 12412 |
. . . . . 6
⊢ (4 + 1) =
5 |
| 106 | | eqid 2737 |
. . . . . 6
⊢ ;84 = ;84 |
| 107 | 13, 2, 105, 106 | decsuc 12764 |
. . . . 5
⊢ (;84 + 1) = ;85 |
| 108 | 18 | nn0cni 12538 |
. . . . . . 7
⊢ ;32 ∈ ℂ |
| 109 | 108 | addlidi 11449 |
. . . . . 6
⊢ (0 +
;32) = ;32 |
| 110 | 75 | oveq1i 7441 |
. . . . . 6
⊢ ((0
· ;;341) + ;32) = (0 + ;32) |
| 111 | | eqid 2737 |
. . . . . . 7
⊢ ;16 = ;16 |
| 112 | 84 | oveq1i 7441 |
. . . . . . . 8
⊢ ((1
· 2) + 1) = (2 + 1) |
| 113 | | 2p1e3 12408 |
. . . . . . . 8
⊢ (2 + 1) =
3 |
| 114 | 112, 113 | eqtri 2765 |
. . . . . . 7
⊢ ((1
· 2) + 1) = 3 |
| 115 | | 6t2e12 12837 |
. . . . . . 7
⊢ (6
· 2) = ;12 |
| 116 | 17, 7, 20, 111, 17, 7, 114, 115 | decmul1c 12798 |
. . . . . 6
⊢ (;16 · 2) = ;32 |
| 117 | 109, 110,
116 | 3eqtr4i 2775 |
. . . . 5
⊢ ((0
· ;;341) + ;32) = (;16 · 2) |
| 118 | 5, 6, 19, 12, 21, 18, 104, 107, 117 | modxp1i 17108 |
. . . 4
⊢
((2↑;85) mod ;;341) = (;32 mod ;;341) |
| 119 | | eqid 2737 |
. . . . 5
⊢ ;85 = ;85 |
| 120 | | 6p1e7 12414 |
. . . . . 6
⊢ (6 + 1) =
7 |
| 121 | | 8cn 12363 |
. . . . . . 7
⊢ 8 ∈
ℂ |
| 122 | | 8t2e16 12848 |
. . . . . . 7
⊢ (8
· 2) = ;16 |
| 123 | 121, 29, 122 | mulcomli 11270 |
. . . . . 6
⊢ (2
· 8) = ;16 |
| 124 | 7, 20, 120, 123 | decsuc 12764 |
. . . . 5
⊢ ((2
· 8) + 1) = ;17 |
| 125 | 17, 13, 14, 119, 10, 7, 124, 31 | decmul2c 12799 |
. . . 4
⊢ (2
· ;85) = ;;170 |
| 126 | 5, 6, 15, 16, 18, 7, 118, 125, 66 | mod2xi 17107 |
. . 3
⊢
((2↑;;170) mod ;;341) =
(1 mod ;;341) |
| 127 | 17, 9, 10 | decmulnc 12800 |
. . . 4
⊢ (2
· ;;170) = ;(2 · ;17)(2 · 0) |
| 128 | | eqid 2737 |
. . . . . 6
⊢ ;17 = ;17 |
| 129 | 69 | oveq1i 7441 |
. . . . . . 7
⊢ ((2
· 1) + 1) = (2 + 1) |
| 130 | 129, 113 | eqtri 2765 |
. . . . . 6
⊢ ((2
· 1) + 1) = 3 |
| 131 | | 7cn 12360 |
. . . . . . 7
⊢ 7 ∈
ℂ |
| 132 | | 7t2e14 12842 |
. . . . . . 7
⊢ (7
· 2) = ;14 |
| 133 | 131, 29, 132 | mulcomli 11270 |
. . . . . 6
⊢ (2
· 7) = ;14 |
| 134 | 17, 7, 8, 128, 2, 7, 130, 133 | decmul2c 12799 |
. . . . 5
⊢ (2
· ;17) = ;34 |
| 135 | 134, 70 | deceq12i 12742 |
. . . 4
⊢ ;(2 · ;17)(2 · 0) = ;;340 |
| 136 | 127, 135 | eqtri 2765 |
. . 3
⊢ (2
· ;;170) = ;;340 |
| 137 | 5, 6, 11, 12, 7, 7, 126, 136, 78 | mod2xi 17107 |
. 2
⊢
((2↑;;340) mod ;;341) =
(1 mod ;;341) |
| 138 | | 1re 11261 |
. . 3
⊢ 1 ∈
ℝ |
| 139 | | nnrp 13046 |
. . . 4
⊢ (;;341 ∈ ℕ → ;;341
∈ ℝ+) |
| 140 | 5, 139 | ax-mp 5 |
. . 3
⊢ ;;341 ∈ ℝ+ |
| 141 | | 0le1 11786 |
. . 3
⊢ 0 ≤
1 |
| 142 | | 4nn 12349 |
. . . . 5
⊢ 4 ∈
ℕ |
| 143 | 1, 142 | decnncl 12753 |
. . . 4
⊢ ;34 ∈ ℕ |
| 144 | | 9re 12365 |
. . . . 5
⊢ 9 ∈
ℝ |
| 145 | | 1lt9 12472 |
. . . . 5
⊢ 1 <
9 |
| 146 | 138, 144,
145 | ltleii 11384 |
. . . 4
⊢ 1 ≤
9 |
| 147 | 143, 7, 7, 146 | decltdi 12772 |
. . 3
⊢ 1 <
;;341 |
| 148 | | modid 13936 |
. . 3
⊢ (((1
∈ ℝ ∧ ;;341 ∈ ℝ+) ∧
(0 ≤ 1 ∧ 1 < ;;341)) → (1 mod ;;341) =
1) |
| 149 | 138, 140,
141, 147, 148 | mp4an 693 |
. 2
⊢ (1 mod
;;341) = 1 |
| 150 | 137, 149 | eqtri 2765 |
1
⊢
((2↑;;340) mod ;;341) =
1 |