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

Theorem 1259lem3 15771
 Description: Lemma for 1259prm 15774. 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 11259 . . . . . 6 1 ∈ ℕ0
3 2nn0 11260 . . . . . 6 2 ∈ ℕ0
42, 3deccl 11463 . . . . 5 12 ∈ ℕ0
5 5nn0 11263 . . . . 5 5 ∈ ℕ0
64, 5deccl 11463 . . . 4 125 ∈ ℕ0
7 9nn 11143 . . . 4 9 ∈ ℕ
86, 7decnncl 11469 . . 3 1259 ∈ ℕ
91, 8eqeltri 2694 . 2 𝑁 ∈ ℕ
10 2nn 11136 . 2 2 ∈ ℕ
11 3nn0 11261 . . 3 3 ∈ ℕ0
12 8nn0 11266 . . 3 8 ∈ ℕ0
1311, 12deccl 11463 . 2 38 ∈ ℕ0
14 4z 11362 . 2 4 ∈ ℤ
15 7nn0 11265 . . 3 7 ∈ ℕ0
1615, 2deccl 11463 . 2 71 ∈ ℕ0
17 4nn0 11262 . . . 4 4 ∈ ℕ0
1811, 17deccl 11463 . . 3 34 ∈ ℕ0
192, 2deccl 11463 . . . 4 11 ∈ ℕ0
2019nn0zi 11353 . . 3 11 ∈ ℤ
2112, 15deccl 11463 . . . 4 87 ∈ ℕ0
22 0nn0 11258 . . . 4 0 ∈ ℕ0
2321, 22deccl 11463 . . 3 870 ∈ ℕ0
24 6nn0 11264 . . . 4 6 ∈ ℕ0
252, 24deccl 11463 . . 3 16 ∈ ℕ0
2611259lem2 15770 . . 3 ((2↑34) mod 𝑁) = (870 mod 𝑁)
27 2exp4 15725 . . . 4 (2↑4) = 16
2827oveq1i 6620 . . 3 ((2↑4) mod 𝑁) = (16 mod 𝑁)
29 eqid 2621 . . . 4 34 = 34
30 4p4e8 11115 . . . 4 (4 + 4) = 8
3111, 17, 17, 29, 30decaddi 11530 . . 3 (34 + 4) = 38
32 9nn0 11267 . . . . 5 9 ∈ ℕ0
33 eqid 2621 . . . . 5 71 = 71
34 10nn0 11467 . . . . 5 10 ∈ ℕ0
35 eqid 2621 . . . . . 6 11 = 11
3634nn0cni 11255 . . . . . . 7 10 ∈ ℂ
37 7cn 11055 . . . . . . 7 7 ∈ ℂ
38 dec10p 11504 . . . . . . 7 (10 + 7) = 17
3936, 37, 38addcomli 10179 . . . . . 6 (7 + 10) = 17
402, 11deccl 11463 . . . . . 6 13 ∈ ℕ0
416nn0cni 11255 . . . . . . . 8 125 ∈ ℂ
4241mulid2i 9994 . . . . . . 7 (1 · 125) = 125
432dec0h 11473 . . . . . . . 8 1 = 01
44 eqid 2621 . . . . . . . 8 13 = 13
45 0p1e1 11083 . . . . . . . 8 (0 + 1) = 1
46 3cn 11046 . . . . . . . . 9 3 ∈ ℂ
47 ax-1cn 9945 . . . . . . . . 9 1 ∈ ℂ
48 3p1e4 11104 . . . . . . . . 9 (3 + 1) = 4
4946, 47, 48addcomli 10179 . . . . . . . 8 (1 + 3) = 4
5022, 2, 2, 11, 43, 44, 45, 49decadd 11521 . . . . . . 7 (1 + 13) = 14
51 2p1e3 11102 . . . . . . . 8 (2 + 1) = 3
52 eqid 2621 . . . . . . . 8 12 = 12
532, 3, 51, 52decsuc 11486 . . . . . . 7 (12 + 1) = 13
54 5p4e9 11118 . . . . . . 7 (5 + 4) = 9
554, 5, 2, 17, 42, 50, 53, 54decadd 11521 . . . . . 6 ((1 · 125) + (1 + 13)) = 139
56 5cn 11051 . . . . . . . 8 5 ∈ ℂ
57 7p5e12 11558 . . . . . . . 8 (7 + 5) = 12
5837, 56, 57addcomli 10179 . . . . . . 7 (5 + 7) = 12
594, 5, 15, 42, 53, 3, 58decaddci 11531 . . . . . 6 ((1 · 125) + 7) = 132
602, 2, 2, 15, 35, 39, 6, 3, 40, 55, 59decmac 11517 . . . . 5 ((11 · 125) + (7 + 10)) = 1392
61 9p1e10 11447 . . . . . 6 (9 + 1) = 10
62 9cn 11059 . . . . . . 7 9 ∈ ℂ
6319nn0cni 11255 . . . . . . 7 11 ∈ ℂ
64 9t11e99 11622 . . . . . . 7 (9 · 11) = 99
6562, 63, 64mulcomli 9998 . . . . . 6 (11 · 9) = 99
6632, 61, 65decsucc 11501 . . . . 5 ((11 · 9) + 1) = 100
676, 32, 15, 2, 1, 33, 19, 22, 34, 60, 66decma2c 11519 . . . 4 ((11 · 𝑁) + 71) = 13920
68 eqid 2621 . . . . 5 16 = 16
695, 3deccl 11463 . . . . . 6 52 ∈ ℕ0
7069, 3deccl 11463 . . . . 5 522 ∈ ℕ0
71 eqid 2621 . . . . . 6 870 = 870
72 eqid 2621 . . . . . 6 522 = 522
73 eqid 2621 . . . . . . 7 87 = 87
7469nn0cni 11255 . . . . . . . 8 52 ∈ ℂ
7574addid1i 10174 . . . . . . 7 (52 + 0) = 52
76 8cn 11057 . . . . . . . . . 10 8 ∈ ℂ
7776mulid1i 9993 . . . . . . . . 9 (8 · 1) = 8
7856addid1i 10174 . . . . . . . . 9 (5 + 0) = 5
7977, 78oveq12i 6622 . . . . . . . 8 ((8 · 1) + (5 + 0)) = (8 + 5)
80 8p5e13 11566 . . . . . . . 8 (8 + 5) = 13
8179, 80eqtri 2643 . . . . . . 7 ((8 · 1) + (5 + 0)) = 13
8237mulid1i 9993 . . . . . . . . 9 (7 · 1) = 7
8382oveq1i 6620 . . . . . . . 8 ((7 · 1) + 2) = (7 + 2)
84 7p2e9 11123 . . . . . . . 8 (7 + 2) = 9
8532dec0h 11473 . . . . . . . 8 9 = 09
8683, 84, 853eqtri 2647 . . . . . . 7 ((7 · 1) + 2) = 09
8712, 15, 5, 3, 73, 75, 2, 32, 22, 81, 86decmac 11517 . . . . . 6 ((87 · 1) + (52 + 0)) = 139
8847mul02i 10176 . . . . . . . 8 (0 · 1) = 0
8988oveq1i 6620 . . . . . . 7 ((0 · 1) + 2) = (0 + 2)
90 2cn 11042 . . . . . . . 8 2 ∈ ℂ
9190addid2i 10175 . . . . . . 7 (0 + 2) = 2
923dec0h 11473 . . . . . . 7 2 = 02
9389, 91, 923eqtri 2647 . . . . . 6 ((0 · 1) + 2) = 02
9421, 22, 69, 3, 71, 72, 2, 3, 22, 87, 93decmac 11517 . . . . 5 ((870 · 1) + 522) = 1392
95 8t6e48 11610 . . . . . . . 8 (8 · 6) = 48
96 4p1e5 11105 . . . . . . . 8 (4 + 1) = 5
97 8p4e12 11565 . . . . . . . 8 (8 + 4) = 12
9817, 12, 17, 95, 96, 3, 97decaddci 11531 . . . . . . 7 ((8 · 6) + 4) = 52
99 7t6e42 11603 . . . . . . 7 (7 · 6) = 42
10024, 12, 15, 73, 3, 17, 98, 99decmul1c 11538 . . . . . 6 (87 · 6) = 522
101 6cn 11053 . . . . . . 7 6 ∈ ℂ
102101mul02i 10176 . . . . . 6 (0 · 6) = 0
10324, 21, 22, 71, 22, 100, 102decmul1 11536 . . . . 5 (870 · 6) = 5220
10423, 2, 24, 68, 22, 70, 94, 103decmul2c 11540 . . . 4 (870 · 16) = 13920
10567, 104eqtr4i 2646 . . 3 ((11 · 𝑁) + 71) = (870 · 16)
1069, 10, 18, 20, 23, 16, 17, 25, 26, 28, 31, 105modxai 15703 . 2 ((2↑38) mod 𝑁) = (71 mod 𝑁)
107 eqid 2621 . . 3 38 = 38
108 3t2e6 11130 . . . . . 6 (3 · 2) = 6
10946, 90, 108mulcomli 9998 . . . . 5 (2 · 3) = 6
110109oveq1i 6620 . . . 4 ((2 · 3) + 1) = (6 + 1)
111 6p1e7 11107 . . . 4 (6 + 1) = 7
112110, 111eqtri 2643 . . 3 ((2 · 3) + 1) = 7
113 8t2e16 11605 . . . 4 (8 · 2) = 16
11476, 90, 113mulcomli 9998 . . 3 (2 · 8) = 16
1153, 11, 12, 107, 24, 2, 112, 114decmul2c 11540 . 2 (2 · 38) = 76
1165dec0h 11473 . . . 4 5 = 05
117 eqid 2621 . . . . 5 125 = 125
118 4cn 11049 . . . . . . 7 4 ∈ ℂ
119118addid2i 10175 . . . . . 6 (0 + 4) = 4
12017dec0h 11473 . . . . . 6 4 = 04
121119, 120eqtri 2643 . . . . 5 (0 + 4) = 04
12291, 92eqtri 2643 . . . . . 6 (0 + 2) = 02
123118mulid1i 9993 . . . . . . . 8 (4 · 1) = 4
124123, 45oveq12i 6622 . . . . . . 7 ((4 · 1) + (0 + 1)) = (4 + 1)
125124, 96eqtri 2643 . . . . . 6 ((4 · 1) + (0 + 1)) = 5
126 4t2e8 11132 . . . . . . . 8 (4 · 2) = 8
127126oveq1i 6620 . . . . . . 7 ((4 · 2) + 2) = (8 + 2)
128 8p2e10 11561 . . . . . . 7 (8 + 2) = 10
129127, 128eqtri 2643 . . . . . 6 ((4 · 2) + 2) = 10
1302, 3, 22, 3, 52, 122, 17, 22, 2, 125, 129decma2c 11519 . . . . 5 ((4 · 12) + (0 + 2)) = 50
131 5t4e20 11588 . . . . . . 7 (5 · 4) = 20
13256, 118, 131mulcomli 9998 . . . . . 6 (4 · 5) = 20
1333, 22, 17, 132, 119decaddi 11530 . . . . 5 ((4 · 5) + 4) = 24
1344, 5, 22, 17, 117, 121, 17, 17, 3, 130, 133decma2c 11519 . . . 4 ((4 · 125) + (0 + 4)) = 504
135 9t4e36 11616 . . . . . 6 (9 · 4) = 36
13662, 118, 135mulcomli 9998 . . . . 5 (4 · 9) = 36
137 6p5e11 11551 . . . . 5 (6 + 5) = 11
13811, 24, 5, 136, 48, 2, 137decaddci 11531 . . . 4 ((4 · 9) + 5) = 41
1396, 32, 22, 5, 1, 116, 17, 2, 17, 134, 138decma2c 11519 . . 3 ((4 · 𝑁) + 5) = 5041
140 7t7e49 11604 . . . . . 6 (7 · 7) = 49
14117, 96, 140decsucc 11501 . . . . 5 ((7 · 7) + 1) = 50
14237mulid2i 9994 . . . . . . 7 (1 · 7) = 7
143142oveq1i 6620 . . . . . 6 ((1 · 7) + 7) = (7 + 7)
144 7p7e14 11560 . . . . . 6 (7 + 7) = 14
145143, 144eqtri 2643 . . . . 5 ((1 · 7) + 7) = 14
14615, 2, 15, 33, 15, 17, 2, 141, 145decrmac 11528 . . . 4 ((71 · 7) + 7) = 504
14716nn0cni 11255 . . . . 5 71 ∈ ℂ
148147mulid1i 9993 . . . 4 (71 · 1) = 71
14916, 15, 2, 33, 2, 15, 146, 148decmul2c 11540 . . 3 (71 · 71) = 5041
150139, 149eqtr4i 2646 . 2 ((4 · 𝑁) + 5) = (71 · 71)
1519, 10, 13, 14, 16, 5, 106, 115, 150mod2xi 15704 1 ((2↑76) mod 𝑁) = (5 mod 𝑁)
 Colors of variables: wff setvar class Syntax hints:   = wceq 1480  (class class class)co 6610  0cc0 9887  1c1 9888   + caddc 9890   · cmul 9892  ℕcn 10971  2c2 11021  3c3 11022  4c4 11023  5c5 11024  6c6 11025  7c7 11026  8c8 11027  9c9 11028  ;cdc 11444   mod cmo 12615  ↑cexp 12807 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964  ax-pre-sup 9965 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-er 7694  df-en 7907  df-dom 7908  df-sdom 7909  df-sup 8299  df-inf 8300  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-div 10636  df-nn 10972  df-2 11030  df-3 11031  df-4 11032  df-5 11033  df-6 11034  df-7 11035  df-8 11036  df-9 11037  df-n0 11244  df-z 11329  df-dec 11445  df-uz 11639  df-rp 11784  df-fl 12540  df-mod 12616  df-seq 12749  df-exp 12808 This theorem is referenced by:  1259lem4  15772
 Copyright terms: Public domain W3C validator