MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1259lem3 Structured version   Visualization version   GIF version

Theorem 1259lem3 16457
Description: Lemma for 1259prm 16460. Calculate a power mod. In decimal, we calculate 2↑38 = 2↑34 · 2↑4≡870 · 16 = 11𝑁 + 71 and 2↑76 = (2↑34)↑2≡71↑2 = 4𝑁 + 5≡5. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
Hypothesis
Ref Expression
1259prm.1 𝑁 = 1259
Assertion
Ref Expression
1259lem3 ((2↑76) mod 𝑁) = (5 mod 𝑁)

Proof of Theorem 1259lem3
StepHypRef Expression
1 1259prm.1 . . 3 𝑁 = 1259
2 1nn0 11901 . . . . . 6 1 ∈ ℕ0
3 2nn0 11902 . . . . . 6 2 ∈ ℕ0
42, 3deccl 12101 . . . . 5 12 ∈ ℕ0
5 5nn0 11905 . . . . 5 5 ∈ ℕ0
64, 5deccl 12101 . . . 4 125 ∈ ℕ0
7 9nn 11723 . . . 4 9 ∈ ℕ
86, 7decnncl 12106 . . 3 1259 ∈ ℕ
91, 8eqeltri 2910 . 2 𝑁 ∈ ℕ
10 2nn 11698 . 2 2 ∈ ℕ
11 3nn0 11903 . . 3 3 ∈ ℕ0
12 8nn0 11908 . . 3 8 ∈ ℕ0
1311, 12deccl 12101 . 2 38 ∈ ℕ0
14 4z 12004 . 2 4 ∈ ℤ
15 7nn0 11907 . . 3 7 ∈ ℕ0
1615, 2deccl 12101 . 2 71 ∈ ℕ0
17 4nn0 11904 . . . 4 4 ∈ ℕ0
1811, 17deccl 12101 . . 3 34 ∈ ℕ0
192, 2deccl 12101 . . . 4 11 ∈ ℕ0
2019nn0zi 11995 . . 3 11 ∈ ℤ
2112, 15deccl 12101 . . . 4 87 ∈ ℕ0
22 0nn0 11900 . . . 4 0 ∈ ℕ0
2321, 22deccl 12101 . . 3 870 ∈ ℕ0
24 6nn0 11906 . . . 4 6 ∈ ℕ0
252, 24deccl 12101 . . 3 16 ∈ ℕ0
2611259lem2 16456 . . 3 ((2↑34) mod 𝑁) = (870 mod 𝑁)
27 2exp4 16410 . . . 4 (2↑4) = 16
2827oveq1i 7150 . . 3 ((2↑4) mod 𝑁) = (16 mod 𝑁)
29 eqid 2822 . . . 4 34 = 34
30 4p4e8 11780 . . . 4 (4 + 4) = 8
3111, 17, 17, 29, 30decaddi 12146 . . 3 (34 + 4) = 38
32 9nn0 11909 . . . . 5 9 ∈ ℕ0
33 eqid 2822 . . . . 5 71 = 71
34 10nn0 12104 . . . . 5 10 ∈ ℕ0
35 eqid 2822 . . . . . 6 11 = 11
3634nn0cni 11897 . . . . . . 7 10 ∈ ℂ
37 7cn 11719 . . . . . . 7 7 ∈ ℂ
38 dec10p 12129 . . . . . . 7 (10 + 7) = 17
3936, 37, 38addcomli 10821 . . . . . 6 (7 + 10) = 17
402, 11deccl 12101 . . . . . 6 13 ∈ ℕ0
416nn0cni 11897 . . . . . . . 8 125 ∈ ℂ
4241mulid2i 10635 . . . . . . 7 (1 · 125) = 125
432dec0h 12108 . . . . . . . 8 1 = 01
44 eqid 2822 . . . . . . . 8 13 = 13
45 0p1e1 11747 . . . . . . . 8 (0 + 1) = 1
46 3cn 11706 . . . . . . . . 9 3 ∈ ℂ
47 ax-1cn 10584 . . . . . . . . 9 1 ∈ ℂ
48 3p1e4 11770 . . . . . . . . 9 (3 + 1) = 4
4946, 47, 48addcomli 10821 . . . . . . . 8 (1 + 3) = 4
5022, 2, 2, 11, 43, 44, 45, 49decadd 12140 . . . . . . 7 (1 + 13) = 14
51 2p1e3 11767 . . . . . . . 8 (2 + 1) = 3
52 eqid 2822 . . . . . . . 8 12 = 12
532, 3, 51, 52decsuc 12117 . . . . . . 7 (12 + 1) = 13
54 5p4e9 11783 . . . . . . 7 (5 + 4) = 9
554, 5, 2, 17, 42, 50, 53, 54decadd 12140 . . . . . 6 ((1 · 125) + (1 + 13)) = 139
56 5cn 11713 . . . . . . . 8 5 ∈ ℂ
57 7p5e12 12163 . . . . . . . 8 (7 + 5) = 12
5837, 56, 57addcomli 10821 . . . . . . 7 (5 + 7) = 12
594, 5, 15, 42, 53, 3, 58decaddci 12147 . . . . . 6 ((1 · 125) + 7) = 132
602, 2, 2, 15, 35, 39, 6, 3, 40, 55, 59decmac 12138 . . . . 5 ((11 · 125) + (7 + 10)) = 1392
61 9p1e10 12088 . . . . . 6 (9 + 1) = 10
62 9cn 11725 . . . . . . 7 9 ∈ ℂ
6319nn0cni 11897 . . . . . . 7 11 ∈ ℂ
64 9t11e99 12216 . . . . . . 7 (9 · 11) = 99
6562, 63, 64mulcomli 10639 . . . . . 6 (11 · 9) = 99
6632, 61, 65decsucc 12127 . . . . 5 ((11 · 9) + 1) = 100
676, 32, 15, 2, 1, 33, 19, 22, 34, 60, 66decma2c 12139 . . . 4 ((11 · 𝑁) + 71) = 13920
68 eqid 2822 . . . . 5 16 = 16
695, 3deccl 12101 . . . . . 6 52 ∈ ℕ0
7069, 3deccl 12101 . . . . 5 522 ∈ ℕ0
71 eqid 2822 . . . . . 6 870 = 870
72 eqid 2822 . . . . . 6 522 = 522
73 eqid 2822 . . . . . . 7 87 = 87
7469nn0cni 11897 . . . . . . . 8 52 ∈ ℂ
7574addid1i 10816 . . . . . . 7 (52 + 0) = 52
76 8cn 11722 . . . . . . . . . 10 8 ∈ ℂ
7776mulid1i 10634 . . . . . . . . 9 (8 · 1) = 8
7856addid1i 10816 . . . . . . . . 9 (5 + 0) = 5
7977, 78oveq12i 7152 . . . . . . . 8 ((8 · 1) + (5 + 0)) = (8 + 5)
80 8p5e13 12169 . . . . . . . 8 (8 + 5) = 13
8179, 80eqtri 2845 . . . . . . 7 ((8 · 1) + (5 + 0)) = 13
8237mulid1i 10634 . . . . . . . . 9 (7 · 1) = 7
8382oveq1i 7150 . . . . . . . 8 ((7 · 1) + 2) = (7 + 2)
84 7p2e9 11786 . . . . . . . 8 (7 + 2) = 9
8532dec0h 12108 . . . . . . . 8 9 = 09
8683, 84, 853eqtri 2849 . . . . . . 7 ((7 · 1) + 2) = 09
8712, 15, 5, 3, 73, 75, 2, 32, 22, 81, 86decmac 12138 . . . . . 6 ((87 · 1) + (52 + 0)) = 139
8847mul02i 10818 . . . . . . . 8 (0 · 1) = 0
8988oveq1i 7150 . . . . . . 7 ((0 · 1) + 2) = (0 + 2)
90 2cn 11700 . . . . . . . 8 2 ∈ ℂ
9190addid2i 10817 . . . . . . 7 (0 + 2) = 2
923dec0h 12108 . . . . . . 7 2 = 02
9389, 91, 923eqtri 2849 . . . . . 6 ((0 · 1) + 2) = 02
9421, 22, 69, 3, 71, 72, 2, 3, 22, 87, 93decmac 12138 . . . . 5 ((870 · 1) + 522) = 1392
95 8t6e48 12205 . . . . . . . 8 (8 · 6) = 48
96 4p1e5 11771 . . . . . . . 8 (4 + 1) = 5
97 8p4e12 12168 . . . . . . . 8 (8 + 4) = 12
9817, 12, 17, 95, 96, 3, 97decaddci 12147 . . . . . . 7 ((8 · 6) + 4) = 52
99 7t6e42 12199 . . . . . . 7 (7 · 6) = 42
10024, 12, 15, 73, 3, 17, 98, 99decmul1c 12151 . . . . . 6 (87 · 6) = 522
101 6cn 11716 . . . . . . 7 6 ∈ ℂ
102101mul02i 10818 . . . . . 6 (0 · 6) = 0
10324, 21, 22, 71, 100, 102decmul1 12150 . . . . 5 (870 · 6) = 5220
10423, 2, 24, 68, 22, 70, 94, 103decmul2c 12152 . . . 4 (870 · 16) = 13920
10567, 104eqtr4i 2848 . . 3 ((11 · 𝑁) + 71) = (870 · 16)
1069, 10, 18, 20, 23, 16, 17, 25, 26, 28, 31, 105modxai 16393 . 2 ((2↑38) mod 𝑁) = (71 mod 𝑁)
107 eqid 2822 . . 3 38 = 38
108 3t2e6 11791 . . . . . 6 (3 · 2) = 6
10946, 90, 108mulcomli 10639 . . . . 5 (2 · 3) = 6
110109oveq1i 7150 . . . 4 ((2 · 3) + 1) = (6 + 1)
111 6p1e7 11773 . . . 4 (6 + 1) = 7
112110, 111eqtri 2845 . . 3 ((2 · 3) + 1) = 7
113 8t2e16 12201 . . . 4 (8 · 2) = 16
11476, 90, 113mulcomli 10639 . . 3 (2 · 8) = 16
1153, 11, 12, 107, 24, 2, 112, 114decmul2c 12152 . 2 (2 · 38) = 76
1165dec0h 12108 . . . 4 5 = 05
117 eqid 2822 . . . . 5 125 = 125
118 4cn 11710 . . . . . . 7 4 ∈ ℂ
119118addid2i 10817 . . . . . 6 (0 + 4) = 4
12017dec0h 12108 . . . . . 6 4 = 04
121119, 120eqtri 2845 . . . . 5 (0 + 4) = 04
12291, 92eqtri 2845 . . . . . 6 (0 + 2) = 02
123118mulid1i 10634 . . . . . . . 8 (4 · 1) = 4
124123, 45oveq12i 7152 . . . . . . 7 ((4 · 1) + (0 + 1)) = (4 + 1)
125124, 96eqtri 2845 . . . . . 6 ((4 · 1) + (0 + 1)) = 5
126 4t2e8 11793 . . . . . . . 8 (4 · 2) = 8
127126oveq1i 7150 . . . . . . 7 ((4 · 2) + 2) = (8 + 2)
128 8p2e10 12166 . . . . . . 7 (8 + 2) = 10
129127, 128eqtri 2845 . . . . . 6 ((4 · 2) + 2) = 10
1302, 3, 22, 3, 52, 122, 17, 22, 2, 125, 129decma2c 12139 . . . . 5 ((4 · 12) + (0 + 2)) = 50
131 5t4e20 12188 . . . . . . 7 (5 · 4) = 20
13256, 118, 131mulcomli 10639 . . . . . 6 (4 · 5) = 20
1333, 22, 17, 132, 119decaddi 12146 . . . . 5 ((4 · 5) + 4) = 24
1344, 5, 22, 17, 117, 121, 17, 17, 3, 130, 133decma2c 12139 . . . 4 ((4 · 125) + (0 + 4)) = 504
135 9t4e36 12210 . . . . . 6 (9 · 4) = 36
13662, 118, 135mulcomli 10639 . . . . 5 (4 · 9) = 36
137 6p5e11 12159 . . . . 5 (6 + 5) = 11
13811, 24, 5, 136, 48, 2, 137decaddci 12147 . . . 4 ((4 · 9) + 5) = 41
1396, 32, 22, 5, 1, 116, 17, 2, 17, 134, 138decma2c 12139 . . 3 ((4 · 𝑁) + 5) = 5041
140 7t7e49 12200 . . . . . 6 (7 · 7) = 49
14117, 96, 140decsucc 12127 . . . . 5 ((7 · 7) + 1) = 50
14237mulid2i 10635 . . . . . . 7 (1 · 7) = 7
143142oveq1i 7150 . . . . . 6 ((1 · 7) + 7) = (7 + 7)
144 7p7e14 12165 . . . . . 6 (7 + 7) = 14
145143, 144eqtri 2845 . . . . 5 ((1 · 7) + 7) = 14
14615, 2, 15, 33, 15, 17, 2, 141, 145decrmac 12144 . . . 4 ((71 · 7) + 7) = 504
14716nn0cni 11897 . . . . 5 71 ∈ ℂ
148147mulid1i 10634 . . . 4 (71 · 1) = 71
14916, 15, 2, 33, 2, 15, 146, 148decmul2c 12152 . . 3 (71 · 71) = 5041
150139, 149eqtr4i 2848 . 2 ((4 · 𝑁) + 5) = (71 · 71)
1519, 10, 13, 14, 16, 5, 106, 115, 150mod2xi 16394 1 ((2↑76) mod 𝑁) = (5 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  (class class class)co 7140  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531  cn 11625  2c2 11680  3c3 11681  4c4 11682  5c5 11683  6c6 11684  7c7 11685  8c8 11686  9c9 11687  cdc 12086   mod cmo 13232  cexp 13425
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rmo 3138  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-om 7566  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-sup 8894  df-inf 8895  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-rp 12378  df-fl 13157  df-mod 13233  df-seq 13365  df-exp 13426
This theorem is referenced by:  1259lem4  16458
  Copyright terms: Public domain W3C validator