Proof of Theorem 1259lem5
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2nn 12340 | . . . 4
⊢ 2 ∈
ℕ | 
| 2 |  | 3nn0 12546 | . . . . 5
⊢ 3 ∈
ℕ0 | 
| 3 |  | 4nn0 12547 | . . . . 5
⊢ 4 ∈
ℕ0 | 
| 4 | 2, 3 | deccl 12750 | . . . 4
⊢ ;34 ∈
ℕ0 | 
| 5 |  | nnexpcl 14116 | . . . 4
⊢ ((2
∈ ℕ ∧ ;34 ∈
ℕ0) → (2↑;34) ∈ ℕ) | 
| 6 | 1, 4, 5 | mp2an 692 | . . 3
⊢
(2↑;34) ∈
ℕ | 
| 7 |  | nnm1nn0 12569 | . . 3
⊢
((2↑;34) ∈
ℕ → ((2↑;34)
− 1) ∈ ℕ0) | 
| 8 | 6, 7 | ax-mp 5 | . 2
⊢
((2↑;34) − 1)
∈ ℕ0 | 
| 9 |  | 8nn0 12551 | . . . 4
⊢ 8 ∈
ℕ0 | 
| 10 |  | 6nn0 12549 | . . . 4
⊢ 6 ∈
ℕ0 | 
| 11 | 9, 10 | deccl 12750 | . . 3
⊢ ;86 ∈
ℕ0 | 
| 12 |  | 9nn0 12552 | . . 3
⊢ 9 ∈
ℕ0 | 
| 13 | 11, 12 | deccl 12750 | . 2
⊢ ;;869 ∈ ℕ0 | 
| 14 |  | 1259prm.1 | . . 3
⊢ 𝑁 = ;;;1259 | 
| 15 |  | 1nn0 12544 | . . . . . 6
⊢ 1 ∈
ℕ0 | 
| 16 |  | 2nn0 12545 | . . . . . 6
⊢ 2 ∈
ℕ0 | 
| 17 | 15, 16 | deccl 12750 | . . . . 5
⊢ ;12 ∈
ℕ0 | 
| 18 |  | 5nn0 12548 | . . . . 5
⊢ 5 ∈
ℕ0 | 
| 19 | 17, 18 | deccl 12750 | . . . 4
⊢ ;;125 ∈ ℕ0 | 
| 20 |  | 9nn 12365 | . . . 4
⊢ 9 ∈
ℕ | 
| 21 | 19, 20 | decnncl 12755 | . . 3
⊢ ;;;1259
∈ ℕ | 
| 22 | 14, 21 | eqeltri 2836 | . 2
⊢ 𝑁 ∈ ℕ | 
| 23 | 14 | 1259lem2 17170 | . . 3
⊢
((2↑;34) mod 𝑁) = (;;870
mod 𝑁) | 
| 24 |  | 6p1e7 12415 | . . . . 5
⊢ (6 + 1) =
7 | 
| 25 |  | eqid 2736 | . . . . 5
⊢ ;86 = ;86 | 
| 26 | 9, 10, 24, 25 | decsuc 12766 | . . . 4
⊢ (;86 + 1) = ;87 | 
| 27 |  | eqid 2736 | . . . 4
⊢ ;;869 = ;;869 | 
| 28 | 11, 26, 27 | decsucc 12776 | . . 3
⊢ (;;869 + 1) = ;;870 | 
| 29 | 22, 6, 15, 13, 23, 28 | modsubi 17111 | . 2
⊢
(((2↑;34) − 1)
mod 𝑁) = (;;869 mod 𝑁) | 
| 30 | 2, 12 | deccl 12750 | . . . 4
⊢ ;39 ∈
ℕ0 | 
| 31 |  | 0nn0 12543 | . . . 4
⊢ 0 ∈
ℕ0 | 
| 32 | 30, 31 | deccl 12750 | . . 3
⊢ ;;390 ∈ ℕ0 | 
| 33 | 9, 12 | deccl 12750 | . . . 4
⊢ ;89 ∈
ℕ0 | 
| 34 | 16, 15 | deccl 12750 | . . . . . 6
⊢ ;21 ∈
ℕ0 | 
| 35 | 15, 2 | deccl 12750 | . . . . . . 7
⊢ ;13 ∈
ℕ0 | 
| 36 | 34 | nn0zi 12644 | . . . . . . . . 9
⊢ ;21 ∈ ℤ | 
| 37 | 35 | nn0zi 12644 | . . . . . . . . 9
⊢ ;13 ∈ ℤ | 
| 38 |  | gcdcom 16551 | . . . . . . . . 9
⊢ ((;21 ∈ ℤ ∧ ;13 ∈ ℤ) → (;21 gcd ;13) = (;13 gcd ;21)) | 
| 39 | 36, 37, 38 | mp2an 692 | . . . . . . . 8
⊢ (;21 gcd ;13) = (;13 gcd ;21) | 
| 40 |  | 3nn 12346 | . . . . . . . . . . 11
⊢ 3 ∈
ℕ | 
| 41 | 15, 40 | decnncl 12755 | . . . . . . . . . 10
⊢ ;13 ∈ ℕ | 
| 42 |  | 8nn 12362 | . . . . . . . . . 10
⊢ 8 ∈
ℕ | 
| 43 |  | eqid 2736 | . . . . . . . . . . 11
⊢ ;13 = ;13 | 
| 44 | 9 | dec0h 12757 | . . . . . . . . . . 11
⊢ 8 = ;08 | 
| 45 |  | ax-1cn 11214 | . . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ | 
| 46 | 45 | mulridi 11266 | . . . . . . . . . . . . 13
⊢ (1
· 1) = 1 | 
| 47 | 45 | addlidi 11450 | . . . . . . . . . . . . 13
⊢ (0 + 1) =
1 | 
| 48 | 46, 47 | oveq12i 7444 | . . . . . . . . . . . 12
⊢ ((1
· 1) + (0 + 1)) = (1 + 1) | 
| 49 |  | 1p1e2 12392 | . . . . . . . . . . . 12
⊢ (1 + 1) =
2 | 
| 50 | 48, 49 | eqtri 2764 | . . . . . . . . . . 11
⊢ ((1
· 1) + (0 + 1)) = 2 | 
| 51 |  | 3cn 12348 | . . . . . . . . . . . . . 14
⊢ 3 ∈
ℂ | 
| 52 | 51 | mulridi 11266 | . . . . . . . . . . . . 13
⊢ (3
· 1) = 3 | 
| 53 | 52 | oveq1i 7442 | . . . . . . . . . . . 12
⊢ ((3
· 1) + 8) = (3 + 8) | 
| 54 |  | 8cn 12364 | . . . . . . . . . . . . 13
⊢ 8 ∈
ℂ | 
| 55 |  | 8p3e11 12816 | . . . . . . . . . . . . 13
⊢ (8 + 3) =
;11 | 
| 56 | 54, 51, 55 | addcomli 11454 | . . . . . . . . . . . 12
⊢ (3 + 8) =
;11 | 
| 57 | 53, 56 | eqtri 2764 | . . . . . . . . . . 11
⊢ ((3
· 1) + 8) = ;11 | 
| 58 | 15, 2, 31, 9, 43, 44, 15, 15, 15, 50, 57 | decmac 12787 | . . . . . . . . . 10
⊢ ((;13 · 1) + 8) = ;21 | 
| 59 |  | 1nn 12278 | . . . . . . . . . . 11
⊢ 1 ∈
ℕ | 
| 60 |  | 8lt10 12867 | . . . . . . . . . . 11
⊢ 8 <
;10 | 
| 61 | 59, 2, 9, 60 | declti 12773 | . . . . . . . . . 10
⊢ 8 <
;13 | 
| 62 | 41, 15, 42, 58, 61 | ndvdsi 16450 | . . . . . . . . 9
⊢  ¬
;13 ∥ ;21 | 
| 63 |  | 13prm 17154 | . . . . . . . . . 10
⊢ ;13 ∈ ℙ | 
| 64 |  | coprm 16749 | . . . . . . . . . 10
⊢ ((;13 ∈ ℙ ∧ ;21 ∈ ℤ) → (¬ ;13 ∥ ;21 ↔ (;13 gcd ;21) = 1)) | 
| 65 | 63, 36, 64 | mp2an 692 | . . . . . . . . 9
⊢ (¬
;13 ∥ ;21 ↔ (;13 gcd ;21) = 1) | 
| 66 | 62, 65 | mpbi 230 | . . . . . . . 8
⊢ (;13 gcd ;21) = 1 | 
| 67 | 39, 66 | eqtri 2764 | . . . . . . 7
⊢ (;21 gcd ;13) = 1 | 
| 68 |  | eqid 2736 | . . . . . . . 8
⊢ ;21 = ;21 | 
| 69 |  | 2cn 12342 | . . . . . . . . . . 11
⊢ 2 ∈
ℂ | 
| 70 | 69 | mullidi 11267 | . . . . . . . . . 10
⊢ (1
· 2) = 2 | 
| 71 | 45 | addridi 11449 | . . . . . . . . . 10
⊢ (1 + 0) =
1 | 
| 72 | 70, 71 | oveq12i 7444 | . . . . . . . . 9
⊢ ((1
· 2) + (1 + 0)) = (2 + 1) | 
| 73 |  | 2p1e3 12409 | . . . . . . . . 9
⊢ (2 + 1) =
3 | 
| 74 | 72, 73 | eqtri 2764 | . . . . . . . 8
⊢ ((1
· 2) + (1 + 0)) = 3 | 
| 75 | 46 | oveq1i 7442 | . . . . . . . . 9
⊢ ((1
· 1) + 3) = (1 + 3) | 
| 76 |  | 3p1e4 12412 | . . . . . . . . . 10
⊢ (3 + 1) =
4 | 
| 77 | 51, 45, 76 | addcomli 11454 | . . . . . . . . 9
⊢ (1 + 3) =
4 | 
| 78 | 3 | dec0h 12757 | . . . . . . . . 9
⊢ 4 = ;04 | 
| 79 | 75, 77, 78 | 3eqtri 2768 | . . . . . . . 8
⊢ ((1
· 1) + 3) = ;04 | 
| 80 | 16, 15, 15, 2, 68, 43, 15, 3, 31, 74, 79 | decma2c 12788 | . . . . . . 7
⊢ ((1
· ;21) + ;13) = ;34 | 
| 81 | 15, 35, 34, 67, 80 | gcdi 17112 | . . . . . 6
⊢ (;34 gcd ;21) = 1 | 
| 82 |  | eqid 2736 | . . . . . . 7
⊢ ;34 = ;34 | 
| 83 |  | 3t2e6 12433 | . . . . . . . . . 10
⊢ (3
· 2) = 6 | 
| 84 | 51, 69, 83 | mulcomli 11271 | . . . . . . . . 9
⊢ (2
· 3) = 6 | 
| 85 | 69 | addridi 11449 | . . . . . . . . 9
⊢ (2 + 0) =
2 | 
| 86 | 84, 85 | oveq12i 7444 | . . . . . . . 8
⊢ ((2
· 3) + (2 + 0)) = (6 + 2) | 
| 87 |  | 6p2e8 12426 | . . . . . . . 8
⊢ (6 + 2) =
8 | 
| 88 | 86, 87 | eqtri 2764 | . . . . . . 7
⊢ ((2
· 3) + (2 + 0)) = 8 | 
| 89 |  | 4cn 12352 | . . . . . . . . . 10
⊢ 4 ∈
ℂ | 
| 90 |  | 4t2e8 12435 | . . . . . . . . . 10
⊢ (4
· 2) = 8 | 
| 91 | 89, 69, 90 | mulcomli 11271 | . . . . . . . . 9
⊢ (2
· 4) = 8 | 
| 92 | 91 | oveq1i 7442 | . . . . . . . 8
⊢ ((2
· 4) + 1) = (8 + 1) | 
| 93 |  | 8p1e9 12417 | . . . . . . . 8
⊢ (8 + 1) =
9 | 
| 94 | 12 | dec0h 12757 | . . . . . . . 8
⊢ 9 = ;09 | 
| 95 | 92, 93, 94 | 3eqtri 2768 | . . . . . . 7
⊢ ((2
· 4) + 1) = ;09 | 
| 96 | 2, 3, 16, 15, 82, 68, 16, 12, 31, 88, 95 | decma2c 12788 | . . . . . 6
⊢ ((2
· ;34) + ;21) = ;89 | 
| 97 | 16, 34, 4, 81, 96 | gcdi 17112 | . . . . 5
⊢ (;89 gcd ;34) = 1 | 
| 98 |  | eqid 2736 | . . . . . 6
⊢ ;89 = ;89 | 
| 99 |  | 4p3e7 12421 | . . . . . . . . 9
⊢ (4 + 3) =
7 | 
| 100 | 89, 51, 99 | addcomli 11454 | . . . . . . . 8
⊢ (3 + 4) =
7 | 
| 101 | 100 | oveq2i 7443 | . . . . . . 7
⊢ ((4
· 8) + (3 + 4)) = ((4 · 8) + 7) | 
| 102 |  | 7nn0 12550 | . . . . . . . 8
⊢ 7 ∈
ℕ0 | 
| 103 |  | 8t4e32 12852 | . . . . . . . . 9
⊢ (8
· 4) = ;32 | 
| 104 | 54, 89, 103 | mulcomli 11271 | . . . . . . . 8
⊢ (4
· 8) = ;32 | 
| 105 |  | 7cn 12361 | . . . . . . . . 9
⊢ 7 ∈
ℂ | 
| 106 |  | 7p2e9 12428 | . . . . . . . . 9
⊢ (7 + 2) =
9 | 
| 107 | 105, 69, 106 | addcomli 11454 | . . . . . . . 8
⊢ (2 + 7) =
9 | 
| 108 | 2, 16, 102, 104, 107 | decaddi 12795 | . . . . . . 7
⊢ ((4
· 8) + 7) = ;39 | 
| 109 | 101, 108 | eqtri 2764 | . . . . . 6
⊢ ((4
· 8) + (3 + 4)) = ;39 | 
| 110 |  | 9cn 12367 | . . . . . . . 8
⊢ 9 ∈
ℂ | 
| 111 |  | 9t4e36 12859 | . . . . . . . 8
⊢ (9
· 4) = ;36 | 
| 112 | 110, 89, 111 | mulcomli 11271 | . . . . . . 7
⊢ (4
· 9) = ;36 | 
| 113 |  | 6p4e10 12807 | . . . . . . 7
⊢ (6 + 4) =
;10 | 
| 114 | 2, 10, 3, 112, 76, 113 | decaddci2 12797 | . . . . . 6
⊢ ((4
· 9) + 4) = ;40 | 
| 115 | 9, 12, 2, 3, 98, 82, 3, 31, 3, 109, 114 | decma2c 12788 | . . . . 5
⊢ ((4
· ;89) + ;34) = ;;390 | 
| 116 | 3, 4, 33, 97, 115 | gcdi 17112 | . . . 4
⊢ (;;390 gcd ;89) = 1 | 
| 117 |  | eqid 2736 | . . . . 5
⊢ ;;390 = ;;390 | 
| 118 |  | eqid 2736 | . . . . . 6
⊢ ;39 = ;39 | 
| 119 | 54 | addridi 11449 | . . . . . . 7
⊢ (8 + 0) =
8 | 
| 120 | 119, 44 | eqtri 2764 | . . . . . 6
⊢ (8 + 0) =
;08 | 
| 121 | 69 | addlidi 11450 | . . . . . . . 8
⊢ (0 + 2) =
2 | 
| 122 | 84, 121 | oveq12i 7444 | . . . . . . 7
⊢ ((2
· 3) + (0 + 2)) = (6 + 2) | 
| 123 | 122, 87 | eqtri 2764 | . . . . . 6
⊢ ((2
· 3) + (0 + 2)) = 8 | 
| 124 |  | 9t2e18 12857 | . . . . . . . 8
⊢ (9
· 2) = ;18 | 
| 125 | 110, 69, 124 | mulcomli 11271 | . . . . . . 7
⊢ (2
· 9) = ;18 | 
| 126 |  | 8p8e16 12821 | . . . . . . 7
⊢ (8 + 8) =
;16 | 
| 127 | 15, 9, 9, 125, 49, 10, 126 | decaddci 12796 | . . . . . 6
⊢ ((2
· 9) + 8) = ;26 | 
| 128 | 2, 12, 31, 9, 118, 120, 16, 10, 16, 123, 127 | decma2c 12788 | . . . . 5
⊢ ((2
· ;39) + (8 + 0)) = ;86 | 
| 129 |  | 2t0e0 12436 | . . . . . . 7
⊢ (2
· 0) = 0 | 
| 130 | 129 | oveq1i 7442 | . . . . . 6
⊢ ((2
· 0) + 9) = (0 + 9) | 
| 131 | 110 | addlidi 11450 | . . . . . 6
⊢ (0 + 9) =
9 | 
| 132 | 130, 131,
94 | 3eqtri 2768 | . . . . 5
⊢ ((2
· 0) + 9) = ;09 | 
| 133 | 30, 31, 9, 12, 117, 98, 16, 12, 31, 128, 132 | decma2c 12788 | . . . 4
⊢ ((2
· ;;390) + ;89) = ;;869 | 
| 134 | 16, 33, 32, 116, 133 | gcdi 17112 | . . 3
⊢ (;;869 gcd ;;390) =
1 | 
| 135 | 30 | nn0cni 12540 | . . . . . . 7
⊢ ;39 ∈ ℂ | 
| 136 | 135 | addridi 11449 | . . . . . 6
⊢ (;39 + 0) = ;39 | 
| 137 | 54 | mullidi 11267 | . . . . . . . 8
⊢ (1
· 8) = 8 | 
| 138 | 137, 76 | oveq12i 7444 | . . . . . . 7
⊢ ((1
· 8) + (3 + 1)) = (8 + 4) | 
| 139 |  | 8p4e12 12817 | . . . . . . 7
⊢ (8 + 4) =
;12 | 
| 140 | 138, 139 | eqtri 2764 | . . . . . 6
⊢ ((1
· 8) + (3 + 1)) = ;12 | 
| 141 |  | 6cn 12358 | . . . . . . . . 9
⊢ 6 ∈
ℂ | 
| 142 | 141 | mullidi 11267 | . . . . . . . 8
⊢ (1
· 6) = 6 | 
| 143 | 142 | oveq1i 7442 | . . . . . . 7
⊢ ((1
· 6) + 9) = (6 + 9) | 
| 144 |  | 9p6e15 12826 | . . . . . . . 8
⊢ (9 + 6) =
;15 | 
| 145 | 110, 141,
144 | addcomli 11454 | . . . . . . 7
⊢ (6 + 9) =
;15 | 
| 146 | 143, 145 | eqtri 2764 | . . . . . 6
⊢ ((1
· 6) + 9) = ;15 | 
| 147 | 9, 10, 2, 12, 25, 136, 15, 18, 15, 140, 146 | decma2c 12788 | . . . . 5
⊢ ((1
· ;86) + (;39 + 0)) = ;;125 | 
| 148 | 110 | mullidi 11267 | . . . . . . 7
⊢ (1
· 9) = 9 | 
| 149 | 148 | oveq1i 7442 | . . . . . 6
⊢ ((1
· 9) + 0) = (9 + 0) | 
| 150 | 110 | addridi 11449 | . . . . . 6
⊢ (9 + 0) =
9 | 
| 151 | 149, 150,
94 | 3eqtri 2768 | . . . . 5
⊢ ((1
· 9) + 0) = ;09 | 
| 152 | 11, 12, 30, 31, 27, 117, 15, 12, 31, 147, 151 | decma2c 12788 | . . . 4
⊢ ((1
· ;;869) + ;;390) =
;;;1259 | 
| 153 | 152, 14 | eqtr4i 2767 | . . 3
⊢ ((1
· ;;869) + ;;390) =
𝑁 | 
| 154 | 15, 32, 13, 134, 153 | gcdi 17112 | . 2
⊢ (𝑁 gcd ;;869) =
1 | 
| 155 | 8, 13, 22, 29, 154 | gcdmodi 17113 | 1
⊢
(((2↑;34) − 1)
gcd 𝑁) = 1 |