Proof of Theorem 2503lem3
| Step | Hyp | Ref
| Expression |
| 1 | | 2nn 12339 |
. . . 4
⊢ 2 ∈
ℕ |
| 2 | | 1nn0 12542 |
. . . . 5
⊢ 1 ∈
ℕ0 |
| 3 | | 8nn0 12549 |
. . . . 5
⊢ 8 ∈
ℕ0 |
| 4 | 2, 3 | deccl 12748 |
. . . 4
⊢ ;18 ∈
ℕ0 |
| 5 | | nnexpcl 14115 |
. . . 4
⊢ ((2
∈ ℕ ∧ ;18 ∈
ℕ0) → (2↑;18) ∈ ℕ) |
| 6 | 1, 4, 5 | mp2an 692 |
. . 3
⊢
(2↑;18) ∈
ℕ |
| 7 | | nnm1nn0 12567 |
. . 3
⊢
((2↑;18) ∈
ℕ → ((2↑;18)
− 1) ∈ ℕ0) |
| 8 | 6, 7 | ax-mp 5 |
. 2
⊢
((2↑;18) − 1)
∈ ℕ0 |
| 9 | | 3nn0 12544 |
. . . 4
⊢ 3 ∈
ℕ0 |
| 10 | 4, 9 | deccl 12748 |
. . 3
⊢ ;;183 ∈ ℕ0 |
| 11 | 10, 2 | deccl 12748 |
. 2
⊢ ;;;1831
∈ ℕ0 |
| 12 | | 2503prm.1 |
. . 3
⊢ 𝑁 = ;;;2503 |
| 13 | | 2nn0 12543 |
. . . . . 6
⊢ 2 ∈
ℕ0 |
| 14 | | 5nn0 12546 |
. . . . . 6
⊢ 5 ∈
ℕ0 |
| 15 | 13, 14 | deccl 12748 |
. . . . 5
⊢ ;25 ∈
ℕ0 |
| 16 | | 0nn0 12541 |
. . . . 5
⊢ 0 ∈
ℕ0 |
| 17 | 15, 16 | deccl 12748 |
. . . 4
⊢ ;;250 ∈ ℕ0 |
| 18 | | 3nn 12345 |
. . . 4
⊢ 3 ∈
ℕ |
| 19 | 17, 18 | decnncl 12753 |
. . 3
⊢ ;;;2503
∈ ℕ |
| 20 | 12, 19 | eqeltri 2837 |
. 2
⊢ 𝑁 ∈ ℕ |
| 21 | 12 | 2503lem1 17174 |
. . 3
⊢
((2↑;18) mod 𝑁) = (;;;1832 mod 𝑁) |
| 22 | | 1p1e2 12391 |
. . . 4
⊢ (1 + 1) =
2 |
| 23 | | eqid 2737 |
. . . 4
⊢ ;;;1831 =
;;;1831 |
| 24 | 10, 2, 22, 23 | decsuc 12764 |
. . 3
⊢ (;;;1831 +
1) = ;;;1832 |
| 25 | 20, 6, 2, 11, 21, 24 | modsubi 17110 |
. 2
⊢
(((2↑;18) − 1)
mod 𝑁) = (;;;1831
mod 𝑁) |
| 26 | | 6nn0 12547 |
. . . . 5
⊢ 6 ∈
ℕ0 |
| 27 | | 7nn0 12548 |
. . . . 5
⊢ 7 ∈
ℕ0 |
| 28 | 26, 27 | deccl 12748 |
. . . 4
⊢ ;67 ∈
ℕ0 |
| 29 | 28, 13 | deccl 12748 |
. . 3
⊢ ;;672 ∈ ℕ0 |
| 30 | | 4nn0 12545 |
. . . . . 6
⊢ 4 ∈
ℕ0 |
| 31 | 30, 3 | deccl 12748 |
. . . . 5
⊢ ;48 ∈
ℕ0 |
| 32 | 31, 27 | deccl 12748 |
. . . 4
⊢ ;;487 ∈ ℕ0 |
| 33 | 4, 14 | deccl 12748 |
. . . . 5
⊢ ;;185 ∈ ℕ0 |
| 34 | 2, 2 | deccl 12748 |
. . . . . . 7
⊢ ;11 ∈
ℕ0 |
| 35 | 34, 27 | deccl 12748 |
. . . . . 6
⊢ ;;117 ∈ ℕ0 |
| 36 | 26, 3 | deccl 12748 |
. . . . . . 7
⊢ ;68 ∈
ℕ0 |
| 37 | | 9nn0 12550 |
. . . . . . . . 9
⊢ 9 ∈
ℕ0 |
| 38 | 30, 37 | deccl 12748 |
. . . . . . . 8
⊢ ;49 ∈
ℕ0 |
| 39 | 2, 37 | deccl 12748 |
. . . . . . . . 9
⊢ ;19 ∈
ℕ0 |
| 40 | 38 | nn0zi 12642 |
. . . . . . . . . . 11
⊢ ;49 ∈ ℤ |
| 41 | 39 | nn0zi 12642 |
. . . . . . . . . . 11
⊢ ;19 ∈ ℤ |
| 42 | | gcdcom 16550 |
. . . . . . . . . . 11
⊢ ((;49 ∈ ℤ ∧ ;19 ∈ ℤ) → (;49 gcd ;19) = (;19 gcd ;49)) |
| 43 | 40, 41, 42 | mp2an 692 |
. . . . . . . . . 10
⊢ (;49 gcd ;19) = (;19 gcd ;49) |
| 44 | | 9nn 12364 |
. . . . . . . . . . . . 13
⊢ 9 ∈
ℕ |
| 45 | 2, 44 | decnncl 12753 |
. . . . . . . . . . . 12
⊢ ;19 ∈ ℕ |
| 46 | | 1nn 12277 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℕ |
| 47 | 2, 46 | decnncl 12753 |
. . . . . . . . . . . 12
⊢ ;11 ∈ ℕ |
| 48 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ ;19 = ;19 |
| 49 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ ;11 = ;11 |
| 50 | | 2cn 12341 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℂ |
| 51 | 50 | mullidi 11266 |
. . . . . . . . . . . . . . 15
⊢ (1
· 2) = 2 |
| 52 | 51, 22 | oveq12i 7443 |
. . . . . . . . . . . . . 14
⊢ ((1
· 2) + (1 + 1)) = (2 + 2) |
| 53 | | 2p2e4 12401 |
. . . . . . . . . . . . . 14
⊢ (2 + 2) =
4 |
| 54 | 52, 53 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ ((1
· 2) + (1 + 1)) = 4 |
| 55 | | 8p1e9 12416 |
. . . . . . . . . . . . . 14
⊢ (8 + 1) =
9 |
| 56 | | 9t2e18 12855 |
. . . . . . . . . . . . . 14
⊢ (9
· 2) = ;18 |
| 57 | 2, 3, 55, 56 | decsuc 12764 |
. . . . . . . . . . . . 13
⊢ ((9
· 2) + 1) = ;19 |
| 58 | 2, 37, 2, 2, 48, 49, 13, 37, 2, 54, 57 | decmac 12785 |
. . . . . . . . . . . 12
⊢ ((;19 · 2) + ;11) = ;49 |
| 59 | | 1lt9 12472 |
. . . . . . . . . . . . 13
⊢ 1 <
9 |
| 60 | 2, 2, 44, 59 | declt 12761 |
. . . . . . . . . . . 12
⊢ ;11 < ;19 |
| 61 | 45, 13, 47, 58, 60 | ndvdsi 16449 |
. . . . . . . . . . 11
⊢ ¬
;19 ∥ ;49 |
| 62 | | 19prm 17155 |
. . . . . . . . . . . 12
⊢ ;19 ∈ ℙ |
| 63 | | coprm 16748 |
. . . . . . . . . . . 12
⊢ ((;19 ∈ ℙ ∧ ;49 ∈ ℤ) → (¬ ;19 ∥ ;49 ↔ (;19 gcd ;49) = 1)) |
| 64 | 62, 40, 63 | mp2an 692 |
. . . . . . . . . . 11
⊢ (¬
;19 ∥ ;49 ↔ (;19 gcd ;49) = 1) |
| 65 | 61, 64 | mpbi 230 |
. . . . . . . . . 10
⊢ (;19 gcd ;49) = 1 |
| 66 | 43, 65 | eqtri 2765 |
. . . . . . . . 9
⊢ (;49 gcd ;19) = 1 |
| 67 | | eqid 2737 |
. . . . . . . . . 10
⊢ ;49 = ;49 |
| 68 | | 4cn 12351 |
. . . . . . . . . . . . 13
⊢ 4 ∈
ℂ |
| 69 | 68 | mullidi 11266 |
. . . . . . . . . . . 12
⊢ (1
· 4) = 4 |
| 70 | 69, 22 | oveq12i 7443 |
. . . . . . . . . . 11
⊢ ((1
· 4) + (1 + 1)) = (4 + 2) |
| 71 | | 4p2e6 12419 |
. . . . . . . . . . 11
⊢ (4 + 2) =
6 |
| 72 | 70, 71 | eqtri 2765 |
. . . . . . . . . 10
⊢ ((1
· 4) + (1 + 1)) = 6 |
| 73 | | 9cn 12366 |
. . . . . . . . . . . . 13
⊢ 9 ∈
ℂ |
| 74 | 73 | mullidi 11266 |
. . . . . . . . . . . 12
⊢ (1
· 9) = 9 |
| 75 | 74 | oveq1i 7441 |
. . . . . . . . . . 11
⊢ ((1
· 9) + 9) = (9 + 9) |
| 76 | | 9p9e18 12827 |
. . . . . . . . . . 11
⊢ (9 + 9) =
;18 |
| 77 | 75, 76 | eqtri 2765 |
. . . . . . . . . 10
⊢ ((1
· 9) + 9) = ;18 |
| 78 | 30, 37, 2, 37, 67, 48, 2, 3, 2,
72, 77 | decma2c 12786 |
. . . . . . . . 9
⊢ ((1
· ;49) + ;19) = ;68 |
| 79 | 2, 39, 38, 66, 78 | gcdi 17111 |
. . . . . . . 8
⊢ (;68 gcd ;49) = 1 |
| 80 | | eqid 2737 |
. . . . . . . . 9
⊢ ;68 = ;68 |
| 81 | | 6cn 12357 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℂ |
| 82 | 81 | mullidi 11266 |
. . . . . . . . . . 11
⊢ (1
· 6) = 6 |
| 83 | | 4p1e5 12412 |
. . . . . . . . . . 11
⊢ (4 + 1) =
5 |
| 84 | 82, 83 | oveq12i 7443 |
. . . . . . . . . 10
⊢ ((1
· 6) + (4 + 1)) = (6 + 5) |
| 85 | | 6p5e11 12806 |
. . . . . . . . . 10
⊢ (6 + 5) =
;11 |
| 86 | 84, 85 | eqtri 2765 |
. . . . . . . . 9
⊢ ((1
· 6) + (4 + 1)) = ;11 |
| 87 | | 8cn 12363 |
. . . . . . . . . . . 12
⊢ 8 ∈
ℂ |
| 88 | 87 | mullidi 11266 |
. . . . . . . . . . 11
⊢ (1
· 8) = 8 |
| 89 | 88 | oveq1i 7441 |
. . . . . . . . . 10
⊢ ((1
· 8) + 9) = (8 + 9) |
| 90 | | 9p8e17 12826 |
. . . . . . . . . . 11
⊢ (9 + 8) =
;17 |
| 91 | 73, 87, 90 | addcomli 11453 |
. . . . . . . . . 10
⊢ (8 + 9) =
;17 |
| 92 | 89, 91 | eqtri 2765 |
. . . . . . . . 9
⊢ ((1
· 8) + 9) = ;17 |
| 93 | 26, 3, 30, 37, 80, 67, 2, 27, 2, 86, 92 | decma2c 12786 |
. . . . . . . 8
⊢ ((1
· ;68) + ;49) = ;;117 |
| 94 | 2, 38, 36, 79, 93 | gcdi 17111 |
. . . . . . 7
⊢ (;;117 gcd ;68) = 1 |
| 95 | | eqid 2737 |
. . . . . . . 8
⊢ ;;117 = ;;117 |
| 96 | | 6p1e7 12414 |
. . . . . . . . . 10
⊢ (6 + 1) =
7 |
| 97 | 27 | dec0h 12755 |
. . . . . . . . . 10
⊢ 7 = ;07 |
| 98 | 96, 97 | eqtri 2765 |
. . . . . . . . 9
⊢ (6 + 1) =
;07 |
| 99 | | 1t1e1 12428 |
. . . . . . . . . . 11
⊢ (1
· 1) = 1 |
| 100 | | 00id 11436 |
. . . . . . . . . . 11
⊢ (0 + 0) =
0 |
| 101 | 99, 100 | oveq12i 7443 |
. . . . . . . . . 10
⊢ ((1
· 1) + (0 + 0)) = (1 + 0) |
| 102 | | ax-1cn 11213 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
| 103 | 102 | addridi 11448 |
. . . . . . . . . 10
⊢ (1 + 0) =
1 |
| 104 | 101, 103 | eqtri 2765 |
. . . . . . . . 9
⊢ ((1
· 1) + (0 + 0)) = 1 |
| 105 | 99 | oveq1i 7441 |
. . . . . . . . . 10
⊢ ((1
· 1) + 7) = (1 + 7) |
| 106 | | 7cn 12360 |
. . . . . . . . . . 11
⊢ 7 ∈
ℂ |
| 107 | | 7p1e8 12415 |
. . . . . . . . . . 11
⊢ (7 + 1) =
8 |
| 108 | 106, 102,
107 | addcomli 11453 |
. . . . . . . . . 10
⊢ (1 + 7) =
8 |
| 109 | 3 | dec0h 12755 |
. . . . . . . . . 10
⊢ 8 = ;08 |
| 110 | 105, 108,
109 | 3eqtri 2769 |
. . . . . . . . 9
⊢ ((1
· 1) + 7) = ;08 |
| 111 | 2, 2, 16, 27, 49, 98, 2, 3, 16, 104, 110 | decma2c 12786 |
. . . . . . . 8
⊢ ((1
· ;11) + (6 + 1)) = ;18 |
| 112 | 106 | mullidi 11266 |
. . . . . . . . . 10
⊢ (1
· 7) = 7 |
| 113 | 112 | oveq1i 7441 |
. . . . . . . . 9
⊢ ((1
· 7) + 8) = (7 + 8) |
| 114 | | 8p7e15 12818 |
. . . . . . . . . 10
⊢ (8 + 7) =
;15 |
| 115 | 87, 106, 114 | addcomli 11453 |
. . . . . . . . 9
⊢ (7 + 8) =
;15 |
| 116 | 113, 115 | eqtri 2765 |
. . . . . . . 8
⊢ ((1
· 7) + 8) = ;15 |
| 117 | 34, 27, 26, 3, 95, 80, 2, 14, 2, 111, 116 | decma2c 12786 |
. . . . . . 7
⊢ ((1
· ;;117) + ;68) = ;;185 |
| 118 | 2, 36, 35, 94, 117 | gcdi 17111 |
. . . . . 6
⊢ (;;185 gcd ;;117) =
1 |
| 119 | | eqid 2737 |
. . . . . . 7
⊢ ;;185 = ;;185 |
| 120 | | eqid 2737 |
. . . . . . . 8
⊢ ;18 = ;18 |
| 121 | 2, 2, 22, 49 | decsuc 12764 |
. . . . . . . 8
⊢ (;11 + 1) = ;12 |
| 122 | | 2t1e2 12429 |
. . . . . . . . . 10
⊢ (2
· 1) = 2 |
| 123 | 122, 22 | oveq12i 7443 |
. . . . . . . . 9
⊢ ((2
· 1) + (1 + 1)) = (2 + 2) |
| 124 | 123, 53 | eqtri 2765 |
. . . . . . . 8
⊢ ((2
· 1) + (1 + 1)) = 4 |
| 125 | | 8t2e16 12848 |
. . . . . . . . . 10
⊢ (8
· 2) = ;16 |
| 126 | 87, 50, 125 | mulcomli 11270 |
. . . . . . . . 9
⊢ (2
· 8) = ;16 |
| 127 | | 6p2e8 12425 |
. . . . . . . . 9
⊢ (6 + 2) =
8 |
| 128 | 2, 26, 13, 126, 127 | decaddi 12793 |
. . . . . . . 8
⊢ ((2
· 8) + 2) = ;18 |
| 129 | 2, 3, 2, 13, 120, 121, 13, 3, 2, 124, 128 | decma2c 12786 |
. . . . . . 7
⊢ ((2
· ;18) + (;11 + 1)) = ;48 |
| 130 | | 5cn 12354 |
. . . . . . . . 9
⊢ 5 ∈
ℂ |
| 131 | | 5t2e10 12833 |
. . . . . . . . 9
⊢ (5
· 2) = ;10 |
| 132 | 130, 50, 131 | mulcomli 11270 |
. . . . . . . 8
⊢ (2
· 5) = ;10 |
| 133 | 106 | addlidi 11449 |
. . . . . . . 8
⊢ (0 + 7) =
7 |
| 134 | 2, 16, 27, 132, 133 | decaddi 12793 |
. . . . . . 7
⊢ ((2
· 5) + 7) = ;17 |
| 135 | 4, 14, 34, 27, 119, 95, 13, 27, 2, 129, 134 | decma2c 12786 |
. . . . . 6
⊢ ((2
· ;;185) + ;;117) =
;;487 |
| 136 | 13, 35, 33, 118, 135 | gcdi 17111 |
. . . . 5
⊢ (;;487 gcd ;;185) =
1 |
| 137 | | eqid 2737 |
. . . . . 6
⊢ ;;487 = ;;487 |
| 138 | | eqid 2737 |
. . . . . . 7
⊢ ;48 = ;48 |
| 139 | 2, 3, 55, 120 | decsuc 12764 |
. . . . . . 7
⊢ (;18 + 1) = ;19 |
| 140 | 30, 3, 2, 37, 138, 139, 2, 27, 2, 72, 92 | decma2c 12786 |
. . . . . 6
⊢ ((1
· ;48) + (;18 + 1)) = ;67 |
| 141 | 112 | oveq1i 7441 |
. . . . . . 7
⊢ ((1
· 7) + 5) = (7 + 5) |
| 142 | | 7p5e12 12810 |
. . . . . . 7
⊢ (7 + 5) =
;12 |
| 143 | 141, 142 | eqtri 2765 |
. . . . . 6
⊢ ((1
· 7) + 5) = ;12 |
| 144 | 31, 27, 4, 14, 137, 119, 2, 13, 2, 140, 143 | decma2c 12786 |
. . . . 5
⊢ ((1
· ;;487) + ;;185) =
;;672 |
| 145 | 2, 33, 32, 136, 144 | gcdi 17111 |
. . . 4
⊢ (;;672 gcd ;;487) =
1 |
| 146 | | eqid 2737 |
. . . . 5
⊢ ;;672 = ;;672 |
| 147 | | eqid 2737 |
. . . . . 6
⊢ ;67 = ;67 |
| 148 | 30, 3, 55, 138 | decsuc 12764 |
. . . . . 6
⊢ (;48 + 1) = ;49 |
| 149 | 71 | oveq2i 7442 |
. . . . . . 7
⊢ ((2
· 6) + (4 + 2)) = ((2 · 6) + 6) |
| 150 | | 6t2e12 12837 |
. . . . . . . . 9
⊢ (6
· 2) = ;12 |
| 151 | 81, 50, 150 | mulcomli 11270 |
. . . . . . . 8
⊢ (2
· 6) = ;12 |
| 152 | 81, 50, 127 | addcomli 11453 |
. . . . . . . 8
⊢ (2 + 6) =
8 |
| 153 | 2, 13, 26, 151, 152 | decaddi 12793 |
. . . . . . 7
⊢ ((2
· 6) + 6) = ;18 |
| 154 | 149, 153 | eqtri 2765 |
. . . . . 6
⊢ ((2
· 6) + (4 + 2)) = ;18 |
| 155 | | 7t2e14 12842 |
. . . . . . . 8
⊢ (7
· 2) = ;14 |
| 156 | 106, 50, 155 | mulcomli 11270 |
. . . . . . 7
⊢ (2
· 7) = ;14 |
| 157 | | 9p4e13 12822 |
. . . . . . . 8
⊢ (9 + 4) =
;13 |
| 158 | 73, 68, 157 | addcomli 11453 |
. . . . . . 7
⊢ (4 + 9) =
;13 |
| 159 | 2, 30, 37, 156, 22, 9, 158 | decaddci 12794 |
. . . . . 6
⊢ ((2
· 7) + 9) = ;23 |
| 160 | 26, 27, 30, 37, 147, 148, 13, 9, 13, 154, 159 | decma2c 12786 |
. . . . 5
⊢ ((2
· ;67) + (;48 + 1)) = ;;183 |
| 161 | | 2t2e4 12430 |
. . . . . . 7
⊢ (2
· 2) = 4 |
| 162 | 161 | oveq1i 7441 |
. . . . . 6
⊢ ((2
· 2) + 7) = (4 + 7) |
| 163 | | 7p4e11 12809 |
. . . . . . 7
⊢ (7 + 4) =
;11 |
| 164 | 106, 68, 163 | addcomli 11453 |
. . . . . 6
⊢ (4 + 7) =
;11 |
| 165 | 162, 164 | eqtri 2765 |
. . . . 5
⊢ ((2
· 2) + 7) = ;11 |
| 166 | 28, 13, 31, 27, 146, 137, 13, 2, 2, 160, 165 | decma2c 12786 |
. . . 4
⊢ ((2
· ;;672) + ;;487) =
;;;1831 |
| 167 | 13, 32, 29, 145, 166 | gcdi 17111 |
. . 3
⊢ (;;;1831
gcd ;;672) = 1 |
| 168 | | eqid 2737 |
. . . . . 6
⊢ ;;183 = ;;183 |
| 169 | 28 | nn0cni 12538 |
. . . . . . 7
⊢ ;67 ∈ ℂ |
| 170 | 169 | addridi 11448 |
. . . . . 6
⊢ (;67 + 0) = ;67 |
| 171 | 102 | addlidi 11449 |
. . . . . . . . 9
⊢ (0 + 1) =
1 |
| 172 | 99, 171 | oveq12i 7443 |
. . . . . . . 8
⊢ ((1
· 1) + (0 + 1)) = (1 + 1) |
| 173 | 172, 22 | eqtri 2765 |
. . . . . . 7
⊢ ((1
· 1) + (0 + 1)) = 2 |
| 174 | 88 | oveq1i 7441 |
. . . . . . . 8
⊢ ((1
· 8) + 7) = (8 + 7) |
| 175 | 174, 114 | eqtri 2765 |
. . . . . . 7
⊢ ((1
· 8) + 7) = ;15 |
| 176 | 2, 3, 16, 27, 120, 98, 2, 14, 2, 173, 175 | decma2c 12786 |
. . . . . 6
⊢ ((1
· ;18) + (6 + 1)) = ;25 |
| 177 | | 3cn 12347 |
. . . . . . . . 9
⊢ 3 ∈
ℂ |
| 178 | 177 | mullidi 11266 |
. . . . . . . 8
⊢ (1
· 3) = 3 |
| 179 | 178 | oveq1i 7441 |
. . . . . . 7
⊢ ((1
· 3) + 7) = (3 + 7) |
| 180 | | 7p3e10 12808 |
. . . . . . . 8
⊢ (7 + 3) =
;10 |
| 181 | 106, 177,
180 | addcomli 11453 |
. . . . . . 7
⊢ (3 + 7) =
;10 |
| 182 | 179, 181 | eqtri 2765 |
. . . . . 6
⊢ ((1
· 3) + 7) = ;10 |
| 183 | 4, 9, 26, 27, 168, 170, 2, 16, 2, 176, 182 | decma2c 12786 |
. . . . 5
⊢ ((1
· ;;183) + (;67 + 0)) = ;;250 |
| 184 | 99 | oveq1i 7441 |
. . . . . 6
⊢ ((1
· 1) + 2) = (1 + 2) |
| 185 | | 1p2e3 12409 |
. . . . . 6
⊢ (1 + 2) =
3 |
| 186 | 9 | dec0h 12755 |
. . . . . 6
⊢ 3 = ;03 |
| 187 | 184, 185,
186 | 3eqtri 2769 |
. . . . 5
⊢ ((1
· 1) + 2) = ;03 |
| 188 | 10, 2, 28, 13, 23, 146, 2, 9, 16, 183, 187 | decma2c 12786 |
. . . 4
⊢ ((1
· ;;;1831)
+ ;;672) = ;;;2503 |
| 189 | 188, 12 | eqtr4i 2768 |
. . 3
⊢ ((1
· ;;;1831)
+ ;;672) = 𝑁 |
| 190 | 2, 29, 11, 167, 189 | gcdi 17111 |
. 2
⊢ (𝑁 gcd ;;;1831) = 1 |
| 191 | 8, 11, 20, 25, 190 | gcdmodi 17112 |
1
⊢
(((2↑;18) − 1)
gcd 𝑁) = 1 |