ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fermltl GIF version

Theorem fermltl 12160
Description: Fermat's little theorem. When 𝑃 is prime, 𝐴𝑃𝐴 (mod 𝑃) for any 𝐴, see theorem 5.19 in [ApostolNT] p. 114. (Contributed by Mario Carneiro, 28-Feb-2014.) (Proof shortened by AV, 19-Mar-2022.)
Assertion
Ref Expression
fermltl ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝐴𝑃) mod 𝑃) = (𝐴 mod 𝑃))

Proof of Theorem fermltl
StepHypRef Expression
1 prmnn 12036 . . . 4 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
2 dvdsmodexp 11729 . . . . 5 ((𝑃 ∈ ℕ ∧ 𝑃 ∈ ℕ ∧ 𝑃𝐴) → ((𝐴𝑃) mod 𝑃) = (𝐴 mod 𝑃))
323exp 1191 . . . 4 (𝑃 ∈ ℕ → (𝑃 ∈ ℕ → (𝑃𝐴 → ((𝐴𝑃) mod 𝑃) = (𝐴 mod 𝑃))))
41, 1, 3sylc 62 . . 3 (𝑃 ∈ ℙ → (𝑃𝐴 → ((𝐴𝑃) mod 𝑃) = (𝐴 mod 𝑃)))
54adantr 274 . 2 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃𝐴 → ((𝐴𝑃) mod 𝑃) = (𝐴 mod 𝑃)))
6 coprm 12070 . . . 4 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (¬ 𝑃𝐴 ↔ (𝑃 gcd 𝐴) = 1))
7 prmz 12037 . . . . . 6 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
8 gcdcom 11900 . . . . . 6 ((𝑃 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑃 gcd 𝐴) = (𝐴 gcd 𝑃))
97, 8sylan 281 . . . . 5 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃 gcd 𝐴) = (𝐴 gcd 𝑃))
109eqeq1d 2173 . . . 4 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝑃 gcd 𝐴) = 1 ↔ (𝐴 gcd 𝑃) = 1))
116, 10bitrd 187 . . 3 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (¬ 𝑃𝐴 ↔ (𝐴 gcd 𝑃) = 1))
12 simp2 987 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → 𝐴 ∈ ℤ)
1313ad2ant1 1007 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → 𝑃 ∈ ℕ)
1413phicld 12144 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → (ϕ‘𝑃) ∈ ℕ)
1514nnnn0d 9161 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → (ϕ‘𝑃) ∈ ℕ0)
16 zexpcl 10464 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (ϕ‘𝑃) ∈ ℕ0) → (𝐴↑(ϕ‘𝑃)) ∈ ℤ)
1712, 15, 16syl2anc 409 . . . . . . 7 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → (𝐴↑(ϕ‘𝑃)) ∈ ℤ)
18 zq 9558 . . . . . . 7 ((𝐴↑(ϕ‘𝑃)) ∈ ℤ → (𝐴↑(ϕ‘𝑃)) ∈ ℚ)
1917, 18syl 14 . . . . . 6 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → (𝐴↑(ϕ‘𝑃)) ∈ ℚ)
20 1z 9211 . . . . . . 7 1 ∈ ℤ
21 zq 9558 . . . . . . 7 (1 ∈ ℤ → 1 ∈ ℚ)
2220, 21mp1i 10 . . . . . 6 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → 1 ∈ ℚ)
23 nnq 9565 . . . . . . 7 (𝑃 ∈ ℕ → 𝑃 ∈ ℚ)
2413, 23syl 14 . . . . . 6 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → 𝑃 ∈ ℚ)
2513nngt0d 8895 . . . . . 6 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → 0 < 𝑃)
26 eulerth 12159 . . . . . . 7 ((𝑃 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → ((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃))
271, 26syl3an1 1260 . . . . . 6 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → ((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃))
2819, 22, 12, 24, 25, 27modqmul1 10306 . . . . 5 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → (((𝐴↑(ϕ‘𝑃)) · 𝐴) mod 𝑃) = ((1 · 𝐴) mod 𝑃))
29 phiprm 12149 . . . . . . . . . 10 (𝑃 ∈ ℙ → (ϕ‘𝑃) = (𝑃 − 1))
30293ad2ant1 1007 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → (ϕ‘𝑃) = (𝑃 − 1))
3130oveq2d 5855 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → (𝐴↑(ϕ‘𝑃)) = (𝐴↑(𝑃 − 1)))
3231oveq1d 5854 . . . . . . 7 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → ((𝐴↑(ϕ‘𝑃)) · 𝐴) = ((𝐴↑(𝑃 − 1)) · 𝐴))
3312zcnd 9308 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → 𝐴 ∈ ℂ)
34 expm1t 10477 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑃 ∈ ℕ) → (𝐴𝑃) = ((𝐴↑(𝑃 − 1)) · 𝐴))
3533, 13, 34syl2anc 409 . . . . . . 7 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → (𝐴𝑃) = ((𝐴↑(𝑃 − 1)) · 𝐴))
3632, 35eqtr4d 2200 . . . . . 6 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → ((𝐴↑(ϕ‘𝑃)) · 𝐴) = (𝐴𝑃))
3736oveq1d 5854 . . . . 5 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → (((𝐴↑(ϕ‘𝑃)) · 𝐴) mod 𝑃) = ((𝐴𝑃) mod 𝑃))
3833mulid2d 7911 . . . . . 6 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → (1 · 𝐴) = 𝐴)
3938oveq1d 5854 . . . . 5 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → ((1 · 𝐴) mod 𝑃) = (𝐴 mod 𝑃))
4028, 37, 393eqtr3d 2205 . . . 4 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → ((𝐴𝑃) mod 𝑃) = (𝐴 mod 𝑃))
41403expia 1194 . . 3 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝑃) = 1 → ((𝐴𝑃) mod 𝑃) = (𝐴 mod 𝑃)))
4211, 41sylbid 149 . 2 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (¬ 𝑃𝐴 → ((𝐴𝑃) mod 𝑃) = (𝐴 mod 𝑃)))
43 dvdsdc 11732 . . . 4 ((𝑃 ∈ ℕ ∧ 𝐴 ∈ ℤ) → DECID 𝑃𝐴)
441, 43sylan 281 . . 3 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → DECID 𝑃𝐴)
45 exmiddc 826 . . 3 (DECID 𝑃𝐴 → (𝑃𝐴 ∨ ¬ 𝑃𝐴))
4644, 45syl 14 . 2 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃𝐴 ∨ ¬ 𝑃𝐴))
475, 42, 46mpjaod 708 1 ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝐴𝑃) mod 𝑃) = (𝐴 mod 𝑃))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wo 698  DECID wdc 824  w3a 967   = wceq 1342  wcel 2135   class class class wbr 3979  cfv 5185  (class class class)co 5839  cc 7745  1c1 7748   · cmul 7752  cmin 8063  cn 8851  0cn0 9108  cz 9185  cq 9551   mod cmo 10251  cexp 10448  cdvds 11721   gcd cgcd 11869  cprime 12033  ϕcphi 12135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-coll 4094  ax-sep 4097  ax-nul 4105  ax-pow 4150  ax-pr 4184  ax-un 4408  ax-setind 4511  ax-iinf 4562  ax-cnex 7838  ax-resscn 7839  ax-1cn 7840  ax-1re 7841  ax-icn 7842  ax-addcl 7843  ax-addrcl 7844  ax-mulcl 7845  ax-mulrcl 7846  ax-addcom 7847  ax-mulcom 7848  ax-addass 7849  ax-mulass 7850  ax-distr 7851  ax-i2m1 7852  ax-0lt1 7853  ax-1rid 7854  ax-0id 7855  ax-rnegex 7856  ax-precex 7857  ax-cnre 7858  ax-pre-ltirr 7859  ax-pre-ltwlin 7860  ax-pre-lttrn 7861  ax-pre-apti 7862  ax-pre-ltadd 7863  ax-pre-mulgt0 7864  ax-pre-mulext 7865  ax-arch 7866  ax-caucvg 7867
This theorem depends on definitions:  df-bi 116  df-stab 821  df-dc 825  df-3or 968  df-3an 969  df-tru 1345  df-fal 1348  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ne 2335  df-nel 2430  df-ral 2447  df-rex 2448  df-reu 2449  df-rmo 2450  df-rab 2451  df-v 2726  df-sbc 2950  df-csb 3044  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3408  df-if 3519  df-pw 3558  df-sn 3579  df-pr 3580  df-op 3582  df-uni 3787  df-int 3822  df-iun 3865  df-br 3980  df-opab 4041  df-mpt 4042  df-tr 4078  df-id 4268  df-po 4271  df-iso 4272  df-iord 4341  df-on 4343  df-ilim 4344  df-suc 4346  df-iom 4565  df-xp 4607  df-rel 4608  df-cnv 4609  df-co 4610  df-dm 4611  df-rn 4612  df-res 4613  df-ima 4614  df-iota 5150  df-fun 5187  df-fn 5188  df-f 5189  df-f1 5190  df-fo 5191  df-f1o 5192  df-fv 5193  df-isom 5194  df-riota 5795  df-ov 5842  df-oprab 5843  df-mpo 5844  df-1st 6103  df-2nd 6104  df-recs 6267  df-irdg 6332  df-frec 6353  df-1o 6378  df-2o 6379  df-oadd 6382  df-er 6495  df-en 6701  df-dom 6702  df-fin 6703  df-sup 6943  df-pnf 7929  df-mnf 7930  df-xr 7931  df-ltxr 7932  df-le 7933  df-sub 8065  df-neg 8066  df-reap 8467  df-ap 8474  df-div 8563  df-inn 8852  df-2 8910  df-3 8911  df-4 8912  df-n0 9109  df-z 9186  df-uz 9461  df-q 9552  df-rp 9584  df-fz 9939  df-fzo 10072  df-fl 10199  df-mod 10252  df-seqfrec 10375  df-exp 10449  df-ihash 10683  df-cj 10778  df-re 10779  df-im 10780  df-rsqrt 10934  df-abs 10935  df-clim 11214  df-proddc 11486  df-dvds 11722  df-gcd 11870  df-prm 12034  df-phi 12137
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator