Metamath Proof Explorer

Theorem hashscontpow

Description: If a set contains all N -th powers, then the size of the image under the ZR homomorphism is greater than the R -th order of N . (Contributed by metakunt, 28-Apr-2025)

Ref Expression
Hypotheses hashscontpow.1 ⊢ ( 𝜑 → 𝐸 ⊆ ℤ )
hashscontpow.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
hashscontpow.3 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( 𝑁 ↑ 𝑘 ) ∈ 𝐸 )
hashscontpow.4 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
hashscontpow.5 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
hashscontpow.6 ⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
hashscontpow.7 ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑅 )
Assertion hashscontpow ( 𝜑 → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ♯ ‘ ( 𝐿 “ 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 hashscontpow.1 ⊢ ( 𝜑 → 𝐸 ⊆ ℤ )
2 hashscontpow.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 hashscontpow.3 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( 𝑁 ↑ 𝑘 ) ∈ 𝐸 )
4 hashscontpow.4 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
5 hashscontpow.5 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
6 hashscontpow.6 ⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
7 hashscontpow.7 ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑅 )
8 2 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
9 odzcl ⊢ ( ( 𝑅 ∈ ℕ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 gcd 𝑅 ) = 1 ) → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℕ )
10 4 8 5 9 syl3anc ⊢ ( 𝜑 → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℕ )
11 10 nnnn0d ⊢ ( 𝜑 → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℕ0 )
12 hashfz1 ⊢ ( ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) = ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
13 11 12 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) = ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
14 ovexd ⊢ ( 𝜑 → ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ∈ V )
15 14 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ∈ V )
16 6 fvexi ⊢ 𝐿 ∈ V
17 16 a1i ⊢ ( 𝜑 → 𝐿 ∈ V )
18 imaexg ⊢ ( 𝐿 ∈ V → ( 𝐿 “ 𝐸 ) ∈ V )
19 17 18 syl ⊢ ( 𝜑 → ( 𝐿 “ 𝐸 ) ∈ V )
20 4 nnnn0d ⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )
21 7 zncrng ⊢ ( 𝑅 ∈ ℕ0 → 𝑌 ∈ CRing )
22 20 21 syl ⊢ ( 𝜑 → 𝑌 ∈ CRing )
23 crngring ⊢ ( 𝑌 ∈ CRing → 𝑌 ∈ Ring )
24 6 zrhrhm ⊢ ( 𝑌 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑌 ) )
25 zringbas ⊢ ℤ = ( Base ‘ ℤring )
26 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
27 25 26 rhmf ⊢ ( 𝐿 ∈ ( ℤring RingHom 𝑌 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) )
28 22 23 24 27 4syl ⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) )
29 28 ffnd ⊢ ( 𝜑 → 𝐿 Fn ℤ )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → 𝐿 Fn ℤ )
31 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → 𝑁 ∈ ℤ )
32 elfznn ⊢ ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) → 𝑥 ∈ ℕ )
33 32 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → 𝑥 ∈ ℕ )
34 33 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → 𝑥 ∈ ℕ0 )
35 31 34 zexpcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → ( 𝑁 ↑ 𝑥 ) ∈ ℤ )
36 oveq2 ⊢ ( 𝑘 = 𝑥 → ( 𝑁 ↑ 𝑘 ) = ( 𝑁 ↑ 𝑥 ) )
37 36 eleq1d ⊢ ( 𝑘 = 𝑥 → ( ( 𝑁 ↑ 𝑘 ) ∈ 𝐸 ↔ ( 𝑁 ↑ 𝑥 ) ∈ 𝐸 ) )
38 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → ∀ 𝑘 ∈ ℕ0 ( 𝑁 ↑ 𝑘 ) ∈ 𝐸 )
39 37 38 34 rspcdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → ( 𝑁 ↑ 𝑥 ) ∈ 𝐸 )
40 30 35 39 fnfvimad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ∈ ( 𝐿 “ 𝐸 ) )
41 40 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) : ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ⟶ ( 𝐿 “ 𝐸 ) )
42 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑎 < 𝑏 ) → 𝑁 ∈ ℕ )
43 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑎 < 𝑏 ) → 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) )
44 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑎 < 𝑏 ) → 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) )
45 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑎 < 𝑏 ) → 𝑅 ∈ ℕ )
46 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑎 < 𝑏 ) → ( 𝑁 gcd 𝑅 ) = 1 )
47 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑎 < 𝑏 ) → 𝑎 < 𝑏 )
48 42 43 44 45 46 6 7 47 hashscontpow1 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑎 < 𝑏 ) → ( 𝐿 ‘ ( 𝑁 ↑ 𝑎 ) ) ≠ ( 𝐿 ‘ ( 𝑁 ↑ 𝑏 ) ) )
49 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 < 𝑎 ) → 𝑁 ∈ ℕ )
50 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 < 𝑎 ) → 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) )
51 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 < 𝑎 ) → 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) )
52 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 < 𝑎 ) → 𝑅 ∈ ℕ )
53 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 < 𝑎 ) → ( 𝑁 gcd 𝑅 ) = 1 )
54 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 < 𝑎 ) → 𝑏 < 𝑎 )
55 49 50 51 52 53 6 7 54 hashscontpow1 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 < 𝑎 ) → ( 𝐿 ‘ ( 𝑁 ↑ 𝑏 ) ) ≠ ( 𝐿 ‘ ( 𝑁 ↑ 𝑎 ) ) )
56 55 necomd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 < 𝑎 ) → ( 𝐿 ‘ ( 𝑁 ↑ 𝑎 ) ) ≠ ( 𝐿 ‘ ( 𝑁 ↑ 𝑏 ) ) )
57 48 56 jaodan ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ ( 𝑎 < 𝑏 ∨ 𝑏 < 𝑎 ) ) → ( 𝐿 ‘ ( 𝑁 ↑ 𝑎 ) ) ≠ ( 𝐿 ‘ ( 𝑁 ↑ 𝑏 ) ) )
58 57 ex ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → ( ( 𝑎 < 𝑏 ∨ 𝑏 < 𝑎 ) → ( 𝐿 ‘ ( 𝑁 ↑ 𝑎 ) ) ≠ ( 𝐿 ‘ ( 𝑁 ↑ 𝑏 ) ) ) )
59 biidd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → ( 𝑎 = 𝑏 ↔ 𝑎 = 𝑏 ) )
60 59 necon3bbid ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → ( ¬ 𝑎 = 𝑏 ↔ 𝑎 ≠ 𝑏 ) )
61 elfzelz ⊢ ( 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) → 𝑎 ∈ ℤ )
62 61 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → 𝑎 ∈ ℤ )
63 62 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → 𝑎 ∈ ℤ )
64 63 zred ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → 𝑎 ∈ ℝ )
65 elfzelz ⊢ ( 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) → 𝑏 ∈ ℤ )
66 65 zred ⊢ ( 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) → 𝑏 ∈ ℝ )
67 66 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → 𝑏 ∈ ℝ )
68 lttri2 ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 𝑎 ≠ 𝑏 ↔ ( 𝑎 < 𝑏 ∨ 𝑏 < 𝑎 ) ) )
69 64 67 68 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → ( 𝑎 ≠ 𝑏 ↔ ( 𝑎 < 𝑏 ∨ 𝑏 < 𝑎 ) ) )
70 60 69 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → ( ¬ 𝑎 = 𝑏 ↔ ( 𝑎 < 𝑏 ∨ 𝑏 < 𝑎 ) ) )
71 70 imbi1d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → ( ( ¬ 𝑎 = 𝑏 → ( 𝐿 ‘ ( 𝑁 ↑ 𝑎 ) ) ≠ ( 𝐿 ‘ ( 𝑁 ↑ 𝑏 ) ) ) ↔ ( ( 𝑎 < 𝑏 ∨ 𝑏 < 𝑎 ) → ( 𝐿 ‘ ( 𝑁 ↑ 𝑎 ) ) ≠ ( 𝐿 ‘ ( 𝑁 ↑ 𝑏 ) ) ) ) )
72 58 71 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → ( ¬ 𝑎 = 𝑏 → ( 𝐿 ‘ ( 𝑁 ↑ 𝑎 ) ) ≠ ( 𝐿 ‘ ( 𝑁 ↑ 𝑏 ) ) ) )
73 72 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ ¬ 𝑎 = 𝑏 ) → ( 𝐿 ‘ ( 𝑁 ↑ 𝑎 ) ) ≠ ( 𝐿 ‘ ( 𝑁 ↑ 𝑏 ) ) )
74 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ ¬ 𝑎 = 𝑏 ) → ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) = ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) )
75 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ ¬ 𝑎 = 𝑏 ) ∧ 𝑥 = 𝑎 ) → 𝑥 = 𝑎 )
76 75 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ ¬ 𝑎 = 𝑏 ) ∧ 𝑥 = 𝑎 ) → ( 𝑁 ↑ 𝑥 ) = ( 𝑁 ↑ 𝑎 ) )
77 76 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ ¬ 𝑎 = 𝑏 ) ∧ 𝑥 = 𝑎 ) → ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝑎 ) ) )
78 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ ¬ 𝑎 = 𝑏 ) → 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) )
79 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ ¬ 𝑎 = 𝑏 ) → ( 𝐿 ‘ ( 𝑁 ↑ 𝑎 ) ) ∈ V )
80 74 77 78 79 fvmptd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ ¬ 𝑎 = 𝑏 ) → ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ‘ 𝑎 ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝑎 ) ) )
81 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ ¬ 𝑎 = 𝑏 ) ∧ 𝑥 = 𝑏 ) → 𝑥 = 𝑏 )
82 81 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ ¬ 𝑎 = 𝑏 ) ∧ 𝑥 = 𝑏 ) → ( 𝑁 ↑ 𝑥 ) = ( 𝑁 ↑ 𝑏 ) )
83 82 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ ¬ 𝑎 = 𝑏 ) ∧ 𝑥 = 𝑏 ) → ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝑏 ) ) )
84 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ ¬ 𝑎 = 𝑏 ) → 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) )
85 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ ¬ 𝑎 = 𝑏 ) → ( 𝐿 ‘ ( 𝑁 ↑ 𝑏 ) ) ∈ V )
86 74 83 84 85 fvmptd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ ¬ 𝑎 = 𝑏 ) → ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ‘ 𝑏 ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝑏 ) ) )
87 80 86 neeq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ ¬ 𝑎 = 𝑏 ) → ( ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ‘ 𝑎 ) ≠ ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ‘ 𝑏 ) ↔ ( 𝐿 ‘ ( 𝑁 ↑ 𝑎 ) ) ≠ ( 𝐿 ‘ ( 𝑁 ↑ 𝑏 ) ) ) )
88 73 87 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ ¬ 𝑎 = 𝑏 ) → ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ‘ 𝑎 ) ≠ ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ‘ 𝑏 ) )
89 88 neneqd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ ¬ 𝑎 = 𝑏 ) → ¬ ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ‘ 𝑎 ) = ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ‘ 𝑏 ) )
90 89 ex ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → ( ¬ 𝑎 = 𝑏 → ¬ ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ‘ 𝑎 ) = ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ‘ 𝑏 ) ) )
91 90 con4d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ∧ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → ( ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ‘ 𝑎 ) = ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
92 91 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) → ∀ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ( ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ‘ 𝑎 ) = ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
93 92 ralrimiva ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ∀ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ( ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ‘ 𝑎 ) = ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
94 41 93 jca ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) : ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ⟶ ( 𝐿 “ 𝐸 ) ∧ ∀ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ∀ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ( ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ‘ 𝑎 ) = ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
95 dff13 ⊢ ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) : ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) –1-1→ ( 𝐿 “ 𝐸 ) ↔ ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) : ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ⟶ ( 𝐿 “ 𝐸 ) ∧ ∀ 𝑎 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ∀ 𝑏 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ( ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ‘ 𝑎 ) = ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
96 94 95 sylibr ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) : ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) –1-1→ ( 𝐿 “ 𝐸 ) )
97 hashf1dmcdm ⊢ ( ( ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) ∈ V ∧ ( 𝐿 “ 𝐸 ) ∈ V ∧ ( 𝑥 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ↦ ( 𝐿 ‘ ( 𝑁 ↑ 𝑥 ) ) ) : ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) –1-1→ ( 𝐿 “ 𝐸 ) ) → ( ♯ ‘ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ≤ ( ♯ ‘ ( 𝐿 “ 𝐸 ) ) )
98 15 19 96 97 syl3anc ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ) ≤ ( ♯ ‘ ( 𝐿 “ 𝐸 ) ) )
99 13 98 eqbrtrrd ⊢ ( 𝜑 → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ♯ ‘ ( 𝐿 “ 𝐸 ) ) )