Metamath Proof Explorer

Theorem znfermltl

Description: Fermat's little theorem in Z/nZ . (Contributed by Thierry Arnoux, 24-Jul-2024)

Ref Expression
Hypotheses znfermltl.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑃 )
znfermltl.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
znfermltl.p ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑍 ) )
Assertion znfermltl ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵 ) → ( 𝑃 ↑ 𝐴 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 znfermltl.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑃 )
2 znfermltl.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
3 znfermltl.p ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑍 ) )
4 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
5 4 nnnn0d ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ0 )
6 5 ad3antrrr ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑎 ∈ ℤ ) ∧ 𝐴 = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) → 𝑃 ∈ ℕ0 )
7 simplr ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑎 ∈ ℤ ) ∧ 𝐴 = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) → 𝑎 ∈ ℤ )
8 eqid ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) = ( ( mulGrp ‘ ℂfld ) ↾s ℤ )
9 zsscn ⊢ ℤ ⊆ ℂ
10 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
11 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
12 10 11 mgpbas ⊢ ℂ = ( Base ‘ ( mulGrp ‘ ℂfld ) )
13 9 12 sseqtri ⊢ ℤ ⊆ ( Base ‘ ( mulGrp ‘ ℂfld ) )
14 eqid ⊢ ( .g ‘ ( mulGrp ‘ ℂfld ) ) = ( .g ‘ ( mulGrp ‘ ℂfld ) )
15 eqid ⊢ ( invg ‘ ( mulGrp ‘ ℂfld ) ) = ( invg ‘ ( mulGrp ‘ ℂfld ) )
16 cnring ⊢ ℂfld ∈ Ring
17 10 ringmgp ⊢ ( ℂfld ∈ Ring → ( mulGrp ‘ ℂfld ) ∈ Mnd )
18 16 17 ax-mp ⊢ ( mulGrp ‘ ℂfld ) ∈ Mnd
19 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
20 10 19 ringidval ⊢ 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
21 1z ⊢ 1 ∈ ℤ
22 20 21 eqeltrri ⊢ ( 0g ‘ ( mulGrp ‘ ℂfld ) ) ∈ ℤ
23 eqid ⊢ ( 0g ‘ ( mulGrp ‘ ℂfld ) ) = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
24 8 12 23 ress0g ⊢ ( ( ( mulGrp ‘ ℂfld ) ∈ Mnd ∧ ( 0g ‘ ( mulGrp ‘ ℂfld ) ) ∈ ℤ ∧ ℤ ⊆ ℂ ) → ( 0g ‘ ( mulGrp ‘ ℂfld ) ) = ( 0g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) ) )
25 18 22 9 24 mp3an ⊢ ( 0g ‘ ( mulGrp ‘ ℂfld ) ) = ( 0g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) )
26 8 13 14 15 25 ressmulgnn0 ⊢ ( ( 𝑃 ∈ ℕ0 ∧ 𝑎 ∈ ℤ ) → ( 𝑃 ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) ) 𝑎 ) = ( 𝑃 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑎 ) )
27 6 7 26 syl2anc ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑎 ∈ ℤ ) ∧ 𝐴 = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) → ( 𝑃 ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) ) 𝑎 ) = ( 𝑃 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑎 ) )
28 7 zcnd ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑎 ∈ ℤ ) ∧ 𝐴 = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) → 𝑎 ∈ ℂ )
29 cnfldexp ⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑃 ∈ ℕ0 ) → ( 𝑃 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑎 ) = ( 𝑎 ↑ 𝑃 ) )
30 28 6 29 syl2anc ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑎 ∈ ℤ ) ∧ 𝐴 = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) → ( 𝑃 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑎 ) = ( 𝑎 ↑ 𝑃 ) )
31 27 30 eqtrd ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑎 ∈ ℤ ) ∧ 𝐴 = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) → ( 𝑃 ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) ) 𝑎 ) = ( 𝑎 ↑ 𝑃 ) )
32 31 fveq2d ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑎 ∈ ℤ ) ∧ 𝐴 = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) → ( ( ℤRHom ‘ 𝑍 ) ‘ ( 𝑃 ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) ) 𝑎 ) ) = ( ( ℤRHom ‘ 𝑍 ) ‘ ( 𝑎 ↑ 𝑃 ) ) )
33 nnnn0 ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℕ0 )
34 1 zncrng ⊢ ( 𝑃 ∈ ℕ0 → 𝑍 ∈ CRing )
35 34 crngringd ⊢ ( 𝑃 ∈ ℕ0 → 𝑍 ∈ Ring )
36 eqid ⊢ ( ℤRHom ‘ 𝑍 ) = ( ℤRHom ‘ 𝑍 )
37 36 zrhrhm ⊢ ( 𝑍 ∈ Ring → ( ℤRHom ‘ 𝑍 ) ∈ ( ℤring RingHom 𝑍 ) )
38 35 37 syl ⊢ ( 𝑃 ∈ ℕ0 → ( ℤRHom ‘ 𝑍 ) ∈ ( ℤring RingHom 𝑍 ) )
39 zringmpg ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) = ( mulGrp ‘ ℤring )
40 eqid ⊢ ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 )
41 39 40 rhmmhm ⊢ ( ( ℤRHom ‘ 𝑍 ) ∈ ( ℤring RingHom 𝑍 ) → ( ℤRHom ‘ 𝑍 ) ∈ ( ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) MndHom ( mulGrp ‘ 𝑍 ) ) )
42 4 33 38 41 4syl ⊢ ( 𝑃 ∈ ℙ → ( ℤRHom ‘ 𝑍 ) ∈ ( ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) MndHom ( mulGrp ‘ 𝑍 ) ) )
43 42 ad3antrrr ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑎 ∈ ℤ ) ∧ 𝐴 = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) → ( ℤRHom ‘ 𝑍 ) ∈ ( ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) MndHom ( mulGrp ‘ 𝑍 ) ) )
44 8 12 ressbas2 ⊢ ( ℤ ⊆ ℂ → ℤ = ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) ) )
45 9 44 ax-mp ⊢ ℤ = ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) )
46 eqid ⊢ ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) ) = ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) )
47 45 46 3 mhmmulg ⊢ ( ( ( ℤRHom ‘ 𝑍 ) ∈ ( ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) MndHom ( mulGrp ‘ 𝑍 ) ) ∧ 𝑃 ∈ ℕ0 ∧ 𝑎 ∈ ℤ ) → ( ( ℤRHom ‘ 𝑍 ) ‘ ( 𝑃 ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) ) 𝑎 ) ) = ( 𝑃 ↑ ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) )
48 43 6 7 47 syl3anc ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑎 ∈ ℤ ) ∧ 𝐴 = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) → ( ( ℤRHom ‘ 𝑍 ) ‘ ( 𝑃 ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) ) 𝑎 ) ) = ( 𝑃 ↑ ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) )
49 simpr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → 𝑎 ∈ ℤ )
50 4 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → 𝑃 ∈ ℕ )
51 50 nnnn0d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → 𝑃 ∈ ℕ0 )
52 zexpcl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑃 ∈ ℕ0 ) → ( 𝑎 ↑ 𝑃 ) ∈ ℤ )
53 49 51 52 syl2anc ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( 𝑎 ↑ 𝑃 ) ∈ ℤ )
54 eqid ⊢ ( -g ‘ ℤring ) = ( -g ‘ ℤring )
55 54 zringsubgval ⊢ ( ( ( 𝑎 ↑ 𝑃 ) ∈ ℤ ∧ 𝑎 ∈ ℤ ) → ( ( 𝑎 ↑ 𝑃 ) − 𝑎 ) = ( ( 𝑎 ↑ 𝑃 ) ( -g ‘ ℤring ) 𝑎 ) )
56 53 49 55 syl2anc ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( ( 𝑎 ↑ 𝑃 ) − 𝑎 ) = ( ( 𝑎 ↑ 𝑃 ) ( -g ‘ ℤring ) 𝑎 ) )
57 56 fveq2d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( ( ℤRHom ‘ 𝑍 ) ‘ ( ( 𝑎 ↑ 𝑃 ) − 𝑎 ) ) = ( ( ℤRHom ‘ 𝑍 ) ‘ ( ( 𝑎 ↑ 𝑃 ) ( -g ‘ ℤring ) 𝑎 ) ) )
58 53 zred ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( 𝑎 ↑ 𝑃 ) ∈ ℝ )
59 zre ⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℝ )
60 59 adantl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → 𝑎 ∈ ℝ )
61 50 nnrpd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → 𝑃 ∈ ℝ+ )
62 fermltl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( ( 𝑎 ↑ 𝑃 ) mod 𝑃 ) = ( 𝑎 mod 𝑃 ) )
63 eqidd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( 𝑎 mod 𝑃 ) = ( 𝑎 mod 𝑃 ) )
64 58 60 60 60 61 62 63 modsub12d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( ( ( 𝑎 ↑ 𝑃 ) − 𝑎 ) mod 𝑃 ) = ( ( 𝑎 − 𝑎 ) mod 𝑃 ) )
65 zcn ⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℂ )
66 65 subidd ⊢ ( 𝑎 ∈ ℤ → ( 𝑎 − 𝑎 ) = 0 )
67 66 adantl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( 𝑎 − 𝑎 ) = 0 )
68 67 oveq1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( ( 𝑎 − 𝑎 ) mod 𝑃 ) = ( 0 mod 𝑃 ) )
69 0mod ⊢ ( 𝑃 ∈ ℝ+ → ( 0 mod 𝑃 ) = 0 )
70 61 69 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( 0 mod 𝑃 ) = 0 )
71 64 68 70 3eqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( ( ( 𝑎 ↑ 𝑃 ) − 𝑎 ) mod 𝑃 ) = 0 )
72 53 49 zsubcld ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( ( 𝑎 ↑ 𝑃 ) − 𝑎 ) ∈ ℤ )
73 dvdsval3 ⊢ ( ( 𝑃 ∈ ℕ ∧ ( ( 𝑎 ↑ 𝑃 ) − 𝑎 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( 𝑎 ↑ 𝑃 ) − 𝑎 ) ↔ ( ( ( 𝑎 ↑ 𝑃 ) − 𝑎 ) mod 𝑃 ) = 0 ) )
74 50 72 73 syl2anc ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( 𝑃 ∥ ( ( 𝑎 ↑ 𝑃 ) − 𝑎 ) ↔ ( ( ( 𝑎 ↑ 𝑃 ) − 𝑎 ) mod 𝑃 ) = 0 ) )
75 71 74 mpbird ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → 𝑃 ∥ ( ( 𝑎 ↑ 𝑃 ) − 𝑎 ) )
76 eqid ⊢ ( 0g ‘ 𝑍 ) = ( 0g ‘ 𝑍 )
77 1 36 76 zndvds0 ⊢ ( ( 𝑃 ∈ ℕ0 ∧ ( ( 𝑎 ↑ 𝑃 ) − 𝑎 ) ∈ ℤ ) → ( ( ( ℤRHom ‘ 𝑍 ) ‘ ( ( 𝑎 ↑ 𝑃 ) − 𝑎 ) ) = ( 0g ‘ 𝑍 ) ↔ 𝑃 ∥ ( ( 𝑎 ↑ 𝑃 ) − 𝑎 ) ) )
78 51 72 77 syl2anc ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( ( ( ℤRHom ‘ 𝑍 ) ‘ ( ( 𝑎 ↑ 𝑃 ) − 𝑎 ) ) = ( 0g ‘ 𝑍 ) ↔ 𝑃 ∥ ( ( 𝑎 ↑ 𝑃 ) − 𝑎 ) ) )
79 75 78 mpbird ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( ( ℤRHom ‘ 𝑍 ) ‘ ( ( 𝑎 ↑ 𝑃 ) − 𝑎 ) ) = ( 0g ‘ 𝑍 ) )
80 rhmghm ⊢ ( ( ℤRHom ‘ 𝑍 ) ∈ ( ℤring RingHom 𝑍 ) → ( ℤRHom ‘ 𝑍 ) ∈ ( ℤring GrpHom 𝑍 ) )
81 51 38 80 3syl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( ℤRHom ‘ 𝑍 ) ∈ ( ℤring GrpHom 𝑍 ) )
82 zringbas ⊢ ℤ = ( Base ‘ ℤring )
83 eqid ⊢ ( -g ‘ 𝑍 ) = ( -g ‘ 𝑍 )
84 82 54 83 ghmsub ⊢ ( ( ( ℤRHom ‘ 𝑍 ) ∈ ( ℤring GrpHom 𝑍 ) ∧ ( 𝑎 ↑ 𝑃 ) ∈ ℤ ∧ 𝑎 ∈ ℤ ) → ( ( ℤRHom ‘ 𝑍 ) ‘ ( ( 𝑎 ↑ 𝑃 ) ( -g ‘ ℤring ) 𝑎 ) ) = ( ( ( ℤRHom ‘ 𝑍 ) ‘ ( 𝑎 ↑ 𝑃 ) ) ( -g ‘ 𝑍 ) ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) )
85 81 53 49 84 syl3anc ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( ( ℤRHom ‘ 𝑍 ) ‘ ( ( 𝑎 ↑ 𝑃 ) ( -g ‘ ℤring ) 𝑎 ) ) = ( ( ( ℤRHom ‘ 𝑍 ) ‘ ( 𝑎 ↑ 𝑃 ) ) ( -g ‘ 𝑍 ) ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) )
86 57 79 85 3eqtr3rd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( ( ( ℤRHom ‘ 𝑍 ) ‘ ( 𝑎 ↑ 𝑃 ) ) ( -g ‘ 𝑍 ) ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) = ( 0g ‘ 𝑍 ) )
87 4 33 35 3syl ⊢ ( 𝑃 ∈ ℙ → 𝑍 ∈ Ring )
88 87 ringgrpd ⊢ ( 𝑃 ∈ ℙ → 𝑍 ∈ Grp )
89 88 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → 𝑍 ∈ Grp )
90 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
91 82 90 rhmf ⊢ ( ( ℤRHom ‘ 𝑍 ) ∈ ( ℤring RingHom 𝑍 ) → ( ℤRHom ‘ 𝑍 ) : ℤ ⟶ ( Base ‘ 𝑍 ) )
92 51 38 91 3syl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( ℤRHom ‘ 𝑍 ) : ℤ ⟶ ( Base ‘ 𝑍 ) )
93 92 53 ffvelrnd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( ( ℤRHom ‘ 𝑍 ) ‘ ( 𝑎 ↑ 𝑃 ) ) ∈ ( Base ‘ 𝑍 ) )
94 92 49 ffvelrnd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝑍 ) )
95 90 76 83 grpsubeq0 ⊢ ( ( 𝑍 ∈ Grp ∧ ( ( ℤRHom ‘ 𝑍 ) ‘ ( 𝑎 ↑ 𝑃 ) ) ∈ ( Base ‘ 𝑍 ) ∧ ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝑍 ) ) → ( ( ( ( ℤRHom ‘ 𝑍 ) ‘ ( 𝑎 ↑ 𝑃 ) ) ( -g ‘ 𝑍 ) ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) = ( 0g ‘ 𝑍 ) ↔ ( ( ℤRHom ‘ 𝑍 ) ‘ ( 𝑎 ↑ 𝑃 ) ) = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) )
96 89 93 94 95 syl3anc ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( ( ( ( ℤRHom ‘ 𝑍 ) ‘ ( 𝑎 ↑ 𝑃 ) ) ( -g ‘ 𝑍 ) ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) = ( 0g ‘ 𝑍 ) ↔ ( ( ℤRHom ‘ 𝑍 ) ‘ ( 𝑎 ↑ 𝑃 ) ) = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) )
97 86 96 mpbid ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℤ ) → ( ( ℤRHom ‘ 𝑍 ) ‘ ( 𝑎 ↑ 𝑃 ) ) = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) )
98 97 ad4ant13 ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑎 ∈ ℤ ) ∧ 𝐴 = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) → ( ( ℤRHom ‘ 𝑍 ) ‘ ( 𝑎 ↑ 𝑃 ) ) = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) )
99 32 48 98 3eqtr3d ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑎 ∈ ℤ ) ∧ 𝐴 = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) → ( 𝑃 ↑ ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) )
100 oveq2 ⊢ ( 𝐴 = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) → ( 𝑃 ↑ 𝐴 ) = ( 𝑃 ↑ ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) )
101 100 adantl ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑎 ∈ ℤ ) ∧ 𝐴 = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) → ( 𝑃 ↑ 𝐴 ) = ( 𝑃 ↑ ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) )
102 simpr ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑎 ∈ ℤ ) ∧ 𝐴 = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) → 𝐴 = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) )
103 99 101 102 3eqtr4d ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑎 ∈ ℤ ) ∧ 𝐴 = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) ) → ( 𝑃 ↑ 𝐴 ) = 𝐴 )
104 1 2 36 znzrhfo ⊢ ( 𝑃 ∈ ℕ0 → ( ℤRHom ‘ 𝑍 ) : ℤ –onto→ 𝐵 )
105 4 33 104 3syl ⊢ ( 𝑃 ∈ ℙ → ( ℤRHom ‘ 𝑍 ) : ℤ –onto→ 𝐵 )
106 foelrn ⊢ ( ( ( ℤRHom ‘ 𝑍 ) : ℤ –onto→ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ∃ 𝑎 ∈ ℤ 𝐴 = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) )
107 105 106 sylan ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵 ) → ∃ 𝑎 ∈ ℤ 𝐴 = ( ( ℤRHom ‘ 𝑍 ) ‘ 𝑎 ) )
108 103 107 r19.29a ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵 ) → ( 𝑃 ↑ 𝐴 ) = 𝐴 )