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

Theorem 2503lem1 16462
Description: Lemma for 2503prm 16465. Calculate a power mod. In decimal, we calculate 2↑18 = 512↑2 = 104𝑁 + 1832≡1832. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
Hypothesis
Ref Expression
2503prm.1 𝑁 = 2503
Assertion
Ref Expression
2503lem1 ((2↑18) mod 𝑁) = (1832 mod 𝑁)

Proof of Theorem 2503lem1
StepHypRef Expression
1 2503prm.1 . . 3 𝑁 = 2503
2 2nn0 11906 . . . . . 6 2 ∈ ℕ0
3 5nn0 11909 . . . . . 6 5 ∈ ℕ0
42, 3deccl 12105 . . . . 5 25 ∈ ℕ0
5 0nn0 11904 . . . . 5 0 ∈ ℕ0
64, 5deccl 12105 . . . 4 250 ∈ ℕ0
7 3nn 11708 . . . 4 3 ∈ ℕ
86, 7decnncl 12110 . . 3 2503 ∈ ℕ
91, 8eqeltri 2913 . 2 𝑁 ∈ ℕ
10 2nn 11702 . 2 2 ∈ ℕ
11 9nn0 11913 . 2 9 ∈ ℕ0
12 10nn0 12108 . . . 4 10 ∈ ℕ0
13 4nn0 11908 . . . 4 4 ∈ ℕ0
1412, 13deccl 12105 . . 3 104 ∈ ℕ0
1514nn0zi 11999 . 2 104 ∈ ℤ
16 1nn0 11905 . . . 4 1 ∈ ℕ0
173, 16deccl 12105 . . 3 51 ∈ ℕ0
1817, 2deccl 12105 . 2 512 ∈ ℕ0
19 8nn0 11912 . . . . 5 8 ∈ ℕ0
2016, 19deccl 12105 . . . 4 18 ∈ ℕ0
21 3nn0 11907 . . . 4 3 ∈ ℕ0
2220, 21deccl 12105 . . 3 183 ∈ ℕ0
2322, 2deccl 12105 . 2 1832 ∈ ℕ0
24 8p1e9 11779 . . . 4 (8 + 1) = 9
25 6nn0 11910 . . . . 5 6 ∈ ℕ0
26 2exp8 16415 . . . . 5 (2↑8) = 256
27 eqid 2825 . . . . . 6 25 = 25
2816dec0h 12112 . . . . . 6 1 = 01
29 2t2e4 11793 . . . . . . . 8 (2 · 2) = 4
30 ax-1cn 10587 . . . . . . . . 9 1 ∈ ℂ
3130addid2i 10820 . . . . . . . 8 (0 + 1) = 1
3229, 31oveq12i 7163 . . . . . . 7 ((2 · 2) + (0 + 1)) = (4 + 1)
33 4p1e5 11775 . . . . . . 7 (4 + 1) = 5
3432, 33eqtri 2848 . . . . . 6 ((2 · 2) + (0 + 1)) = 5
35 5t2e10 12190 . . . . . . 7 (5 · 2) = 10
3616, 5, 31, 35decsuc 12121 . . . . . 6 ((5 · 2) + 1) = 11
372, 3, 5, 16, 27, 28, 2, 16, 16, 34, 36decmac 12142 . . . . 5 ((25 · 2) + 1) = 51
38 6t2e12 12194 . . . . 5 (6 · 2) = 12
392, 4, 25, 26, 2, 16, 37, 38decmul1c 12155 . . . 4 ((2↑8) · 2) = 512
402, 19, 24, 39numexpp1 16406 . . 3 (2↑9) = 512
4140oveq1i 7161 . 2 ((2↑9) mod 𝑁) = (512 mod 𝑁)
42 9cn 11729 . . 3 9 ∈ ℂ
43 2cn 11704 . . 3 2 ∈ ℂ
44 9t2e18 12212 . . 3 (9 · 2) = 18
4542, 43, 44mulcomli 10642 . 2 (2 · 9) = 18
46 eqid 2825 . . . 4 1832 = 1832
4721, 16deccl 12105 . . . 4 31 ∈ ℕ0
482, 16deccl 12105 . . . . 5 21 ∈ ℕ0
49 eqid 2825 . . . . 5 250 = 250
50 eqid 2825 . . . . . 6 183 = 183
51 eqid 2825 . . . . . 6 31 = 31
52 eqid 2825 . . . . . . 7 18 = 18
53 1p1e2 11754 . . . . . . 7 (1 + 1) = 2
54 8p3e11 12171 . . . . . . 7 (8 + 3) = 11
5516, 19, 21, 52, 53, 16, 54decaddci 12151 . . . . . 6 (18 + 3) = 21
56 3p1e4 11774 . . . . . 6 (3 + 1) = 4
5720, 21, 21, 16, 50, 51, 55, 56decadd 12144 . . . . 5 (183 + 31) = 214
5848nn0cni 11901 . . . . . . 7 21 ∈ ℂ
5958addid1i 10819 . . . . . 6 (21 + 0) = 21
603, 2deccl 12105 . . . . . 6 52 ∈ ℕ0
61 eqid 2825 . . . . . . 7 104 = 104
6260nn0cni 11901 . . . . . . . 8 52 ∈ ℂ
63 eqid 2825 . . . . . . . . 9 52 = 52
64 2p2e4 11764 . . . . . . . . 9 (2 + 2) = 4
653, 2, 2, 63, 64decaddi 12150 . . . . . . . 8 (52 + 2) = 54
6662, 43, 65addcomli 10824 . . . . . . 7 (2 + 52) = 54
672dec0u 12111 . . . . . . . . 9 (10 · 2) = 20
68 5p1e6 11776 . . . . . . . . 9 (5 + 1) = 6
6967, 68oveq12i 7163 . . . . . . . 8 ((10 · 2) + (5 + 1)) = (20 + 6)
70 eqid 2825 . . . . . . . . 9 20 = 20
71 6cn 11720 . . . . . . . . . 10 6 ∈ ℂ
7271addid2i 10820 . . . . . . . . 9 (0 + 6) = 6
732, 5, 25, 70, 72decaddi 12150 . . . . . . . 8 (20 + 6) = 26
7469, 73eqtri 2848 . . . . . . 7 ((10 · 2) + (5 + 1)) = 26
75 4t2e8 11797 . . . . . . . . 9 (4 · 2) = 8
7675oveq1i 7161 . . . . . . . 8 ((4 · 2) + 4) = (8 + 4)
77 8p4e12 12172 . . . . . . . 8 (8 + 4) = 12
7876, 77eqtri 2848 . . . . . . 7 ((4 · 2) + 4) = 12
7912, 13, 3, 13, 61, 66, 2, 2, 16, 74, 78decmac 12142 . . . . . 6 ((104 · 2) + (2 + 52)) = 262
803dec0u 12111 . . . . . . . . 9 (10 · 5) = 50
8143addid2i 10820 . . . . . . . . 9 (0 + 2) = 2
8280, 81oveq12i 7163 . . . . . . . 8 ((10 · 5) + (0 + 2)) = (50 + 2)
83 eqid 2825 . . . . . . . . 9 50 = 50
843, 5, 2, 83, 81decaddi 12150 . . . . . . . 8 (50 + 2) = 52
8582, 84eqtri 2848 . . . . . . 7 ((10 · 5) + (0 + 2)) = 52
86 5cn 11717 . . . . . . . . 9 5 ∈ ℂ
87 4cn 11714 . . . . . . . . 9 4 ∈ ℂ
88 5t4e20 12192 . . . . . . . . 9 (5 · 4) = 20
8986, 87, 88mulcomli 10642 . . . . . . . 8 (4 · 5) = 20
902, 5, 31, 89decsuc 12121 . . . . . . 7 ((4 · 5) + 1) = 21
9112, 13, 5, 16, 61, 28, 3, 16, 2, 85, 90decmac 12142 . . . . . 6 ((104 · 5) + 1) = 521
922, 3, 2, 16, 27, 59, 14, 16, 60, 79, 91decma2c 12143 . . . . 5 ((104 · 25) + (21 + 0)) = 2621
9314nn0cni 11901 . . . . . . . 8 104 ∈ ℂ
9493mul01i 10822 . . . . . . 7 (104 · 0) = 0
9594oveq1i 7161 . . . . . 6 ((104 · 0) + 4) = (0 + 4)
9687addid2i 10820 . . . . . 6 (0 + 4) = 4
9713dec0h 12112 . . . . . 6 4 = 04
9895, 96, 973eqtri 2852 . . . . 5 ((104 · 0) + 4) = 04
994, 5, 48, 13, 49, 57, 14, 13, 5, 92, 98decma2c 12143 . . . 4 ((104 · 250) + (183 + 31)) = 26214
100 eqid 2825 . . . . . 6 10 = 10
101 3cn 11710 . . . . . . . . 9 3 ∈ ℂ
102101mulid2i 10638 . . . . . . . 8 (1 · 3) = 3
103 00id 10807 . . . . . . . 8 (0 + 0) = 0
104102, 103oveq12i 7163 . . . . . . 7 ((1 · 3) + (0 + 0)) = (3 + 0)
105101addid1i 10819 . . . . . . 7 (3 + 0) = 3
106104, 105eqtri 2848 . . . . . 6 ((1 · 3) + (0 + 0)) = 3
107101mul02i 10821 . . . . . . . 8 (0 · 3) = 0
108107oveq1i 7161 . . . . . . 7 ((0 · 3) + 1) = (0 + 1)
109108, 31, 283eqtri 2852 . . . . . 6 ((0 · 3) + 1) = 01
11016, 5, 5, 16, 100, 28, 21, 16, 5, 106, 109decmac 12142 . . . . 5 ((10 · 3) + 1) = 31
111 4t3e12 12188 . . . . . 6 (4 · 3) = 12
11216, 2, 2, 111, 64decaddi 12150 . . . . 5 ((4 · 3) + 2) = 14
11312, 13, 2, 61, 21, 13, 16, 110, 112decrmac 12148 . . . 4 ((104 · 3) + 2) = 314
1146, 21, 22, 2, 1, 46, 14, 13, 47, 99, 113decma2c 12143 . . 3 ((104 · 𝑁) + 1832) = 262144
115 eqid 2825 . . . 4 512 = 512
11612, 2deccl 12105 . . . 4 102 ∈ ℕ0
117 eqid 2825 . . . . 5 51 = 51
118 eqid 2825 . . . . 5 102 = 102
11986, 30, 68addcomli 10824 . . . . . . 7 (1 + 5) = 6
12016, 5, 3, 16, 100, 117, 119, 31decadd 12144 . . . . . 6 (10 + 51) = 61
121 7nn0 11911 . . . . . . 7 7 ∈ ℕ0
122 6p1e7 11777 . . . . . . . 8 (6 + 1) = 7
123121dec0h 12112 . . . . . . . 8 7 = 07
124122, 123eqtri 2848 . . . . . . 7 (6 + 1) = 07
12531oveq2i 7162 . . . . . . . 8 ((5 · 5) + (0 + 1)) = ((5 · 5) + 1)
126 5t5e25 12193 . . . . . . . . 9 (5 · 5) = 25
1272, 3, 68, 126decsuc 12121 . . . . . . . 8 ((5 · 5) + 1) = 26
128125, 127eqtri 2848 . . . . . . 7 ((5 · 5) + (0 + 1)) = 26
12986mulid2i 10638 . . . . . . . . 9 (1 · 5) = 5
130129oveq1i 7161 . . . . . . . 8 ((1 · 5) + 7) = (5 + 7)
131 7cn 11723 . . . . . . . . 9 7 ∈ ℂ
132 7p5e12 12167 . . . . . . . . 9 (7 + 5) = 12
133131, 86, 132addcomli 10824 . . . . . . . 8 (5 + 7) = 12
134130, 133eqtri 2848 . . . . . . 7 ((1 · 5) + 7) = 12
1353, 16, 5, 121, 117, 124, 3, 2, 16, 128, 134decmac 12142 . . . . . 6 ((51 · 5) + (6 + 1)) = 262
13686, 43, 35mulcomli 10642 . . . . . . 7 (2 · 5) = 10
13716, 5, 31, 136decsuc 12121 . . . . . 6 ((2 · 5) + 1) = 11
13817, 2, 25, 16, 115, 120, 3, 16, 16, 135, 137decmac 12142 . . . . 5 ((512 · 5) + (10 + 51)) = 2621
13917nn0cni 11901 . . . . . . 7 51 ∈ ℂ
140139mulid1i 10637 . . . . . 6 (51 · 1) = 51
14143mulid1i 10637 . . . . . . . 8 (2 · 1) = 2
142141oveq1i 7161 . . . . . . 7 ((2 · 1) + 2) = (2 + 2)
143142, 64eqtri 2848 . . . . . 6 ((2 · 1) + 2) = 4
14417, 2, 2, 115, 16, 140, 143decrmanc 12147 . . . . 5 ((512 · 1) + 2) = 514
1453, 16, 12, 2, 117, 118, 18, 13, 17, 138, 144decma2c 12143 . . . 4 ((512 · 51) + 102) = 26214
14643mulid2i 10638 . . . . . 6 (1 · 2) = 2
1472, 3, 16, 117, 35, 146decmul1 12154 . . . . 5 (51 · 2) = 102
1482, 17, 2, 115, 147, 29decmul1 12154 . . . 4 (512 · 2) = 1024
14918, 17, 2, 115, 13, 116, 145, 148decmul2c 12156 . . 3 (512 · 512) = 262144
150114, 149eqtr4i 2851 . 2 ((104 · 𝑁) + 1832) = (512 · 512)
1519, 10, 11, 15, 18, 23, 41, 45, 150mod2xi 16397 1 ((2↑18) mod 𝑁) = (1832 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  (class class class)co 7151  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534  cn 11630  2c2 11684  3c3 11685  4c4 11686  5c5 11687  6c6 11688  7c7 11689  8c8 11690  9c9 11691  cdc 12090   mod cmo 13230  cexp 13422
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7572  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-er 8282  df-en 8502  df-dom 8503  df-sdom 8504  df-sup 8898  df-inf 8899  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-rp 12383  df-fl 13155  df-mod 13231  df-seq 13363  df-exp 13423
This theorem is referenced by:  2503lem2  16463  2503lem3  16464
  Copyright terms: Public domain W3C validator