| Step | Hyp | Ref
| Expression |
| 1 | | hashscontpow.4 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ ℕ) |
| 2 | | hashscontpow.2 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 3 | 2 | nnzd 12640 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 4 | | hashscontpow.5 |
. . . . 5
⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) |
| 5 | | odzcl 16831 |
. . . . 5
⊢ ((𝑅 ∈ ℕ ∧ 𝑁 ∈ ℤ ∧ (𝑁 gcd 𝑅) = 1) →
((odℤ‘𝑅)‘𝑁) ∈ ℕ) |
| 6 | 1, 3, 4, 5 | syl3anc 1373 |
. . . 4
⊢ (𝜑 →
((odℤ‘𝑅)‘𝑁) ∈ ℕ) |
| 7 | 6 | nnnn0d 12587 |
. . 3
⊢ (𝜑 →
((odℤ‘𝑅)‘𝑁) ∈
ℕ0) |
| 8 | | hashfz1 14385 |
. . 3
⊢
(((odℤ‘𝑅)‘𝑁) ∈ ℕ0 →
(♯‘(1...((odℤ‘𝑅)‘𝑁))) = ((odℤ‘𝑅)‘𝑁)) |
| 9 | 7, 8 | syl 17 |
. 2
⊢ (𝜑 →
(♯‘(1...((odℤ‘𝑅)‘𝑁))) = ((odℤ‘𝑅)‘𝑁)) |
| 10 | | ovexd 7466 |
. . . 4
⊢ (𝜑 →
(1...((odℤ‘𝑅)‘𝑁)) ∈ V) |
| 11 | 10 | mptexd 7244 |
. . 3
⊢ (𝜑 → (𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥))) ∈ V) |
| 12 | | hashscontpow.6 |
. . . . . 6
⊢ 𝐿 = (ℤRHom‘𝑌) |
| 13 | 12 | fvexi 6920 |
. . . . 5
⊢ 𝐿 ∈ V |
| 14 | 13 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐿 ∈ V) |
| 15 | | imaexg 7935 |
. . . 4
⊢ (𝐿 ∈ V → (𝐿 “ 𝐸) ∈ V) |
| 16 | 14, 15 | syl 17 |
. . 3
⊢ (𝜑 → (𝐿 “ 𝐸) ∈ V) |
| 17 | 1 | nnnn0d 12587 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈
ℕ0) |
| 18 | | hashscontpow.7 |
. . . . . . . . . . . 12
⊢ 𝑌 =
(ℤ/nℤ‘𝑅) |
| 19 | 18 | zncrng 21563 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℕ0
→ 𝑌 ∈
CRing) |
| 20 | 17, 19 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ CRing) |
| 21 | | crngring 20242 |
. . . . . . . . . 10
⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring) |
| 22 | 12 | zrhrhm 21522 |
. . . . . . . . . 10
⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤring
RingHom 𝑌)) |
| 23 | | zringbas 21464 |
. . . . . . . . . . 11
⊢ ℤ =
(Base‘ℤring) |
| 24 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝑌) =
(Base‘𝑌) |
| 25 | 23, 24 | rhmf 20485 |
. . . . . . . . . 10
⊢ (𝐿 ∈ (ℤring
RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌)) |
| 26 | 20, 21, 22, 25 | 4syl 19 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌)) |
| 27 | 26 | ffnd 6737 |
. . . . . . . 8
⊢ (𝜑 → 𝐿 Fn ℤ) |
| 28 | 27 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁))) → 𝐿 Fn ℤ) |
| 29 | 3 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁))) → 𝑁 ∈ ℤ) |
| 30 | | elfznn 13593 |
. . . . . . . . . 10
⊢ (𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) → 𝑥 ∈ ℕ) |
| 31 | 30 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁))) → 𝑥 ∈ ℕ) |
| 32 | 31 | nnnn0d 12587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁))) → 𝑥 ∈ ℕ0) |
| 33 | 29, 32 | zexpcld 14128 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁))) → (𝑁↑𝑥) ∈ ℤ) |
| 34 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑘 = 𝑥 → (𝑁↑𝑘) = (𝑁↑𝑥)) |
| 35 | 34 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑘 = 𝑥 → ((𝑁↑𝑘) ∈ 𝐸 ↔ (𝑁↑𝑥) ∈ 𝐸)) |
| 36 | | hashscontpow.3 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ ℕ0 (𝑁↑𝑘) ∈ 𝐸) |
| 37 | 36 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁))) → ∀𝑘 ∈ ℕ0 (𝑁↑𝑘) ∈ 𝐸) |
| 38 | 35, 37, 32 | rspcdva 3623 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁))) → (𝑁↑𝑥) ∈ 𝐸) |
| 39 | 28, 33, 38 | fnfvimad 7254 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁))) → (𝐿‘(𝑁↑𝑥)) ∈ (𝐿 “ 𝐸)) |
| 40 | 39 | fmpttd 7135 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥))):(1...((odℤ‘𝑅)‘𝑁))⟶(𝐿 “ 𝐸)) |
| 41 | 2 | ad3antrrr 730 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑎 < 𝑏) → 𝑁 ∈ ℕ) |
| 42 | | simpllr 776 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑎 < 𝑏) → 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) |
| 43 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑎 < 𝑏) → 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) |
| 44 | 1 | ad3antrrr 730 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑎 < 𝑏) → 𝑅 ∈ ℕ) |
| 45 | 4 | ad3antrrr 730 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑎 < 𝑏) → (𝑁 gcd 𝑅) = 1) |
| 46 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑎 < 𝑏) → 𝑎 < 𝑏) |
| 47 | 41, 42, 43, 44, 45, 12, 18, 46 | hashscontpow1 42122 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑎 < 𝑏) → (𝐿‘(𝑁↑𝑎)) ≠ (𝐿‘(𝑁↑𝑏))) |
| 48 | 2 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 < 𝑎) → 𝑁 ∈ ℕ) |
| 49 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 < 𝑎) → 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) |
| 50 | | simpllr 776 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 < 𝑎) → 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) |
| 51 | 1 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 < 𝑎) → 𝑅 ∈ ℕ) |
| 52 | 4 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 < 𝑎) → (𝑁 gcd 𝑅) = 1) |
| 53 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 < 𝑎) → 𝑏 < 𝑎) |
| 54 | 48, 49, 50, 51, 52, 12, 18, 53 | hashscontpow1 42122 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 < 𝑎) → (𝐿‘(𝑁↑𝑏)) ≠ (𝐿‘(𝑁↑𝑎))) |
| 55 | 54 | necomd 2996 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 < 𝑎) → (𝐿‘(𝑁↑𝑎)) ≠ (𝐿‘(𝑁↑𝑏))) |
| 56 | 47, 55 | jaodan 960 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ (𝑎 < 𝑏 ∨ 𝑏 < 𝑎)) → (𝐿‘(𝑁↑𝑎)) ≠ (𝐿‘(𝑁↑𝑏))) |
| 57 | 56 | ex 412 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) → ((𝑎 < 𝑏 ∨ 𝑏 < 𝑎) → (𝐿‘(𝑁↑𝑎)) ≠ (𝐿‘(𝑁↑𝑏)))) |
| 58 | | biidd 262 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) → (𝑎 = 𝑏 ↔ 𝑎 = 𝑏)) |
| 59 | 58 | necon3bbid 2978 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) → (¬ 𝑎 = 𝑏 ↔ 𝑎 ≠ 𝑏)) |
| 60 | | elfzelz 13564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁)) → 𝑎 ∈ ℤ) |
| 61 | 60 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) → 𝑎 ∈ ℤ) |
| 62 | 61 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) → 𝑎 ∈ ℤ) |
| 63 | 62 | zred 12722 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) → 𝑎 ∈ ℝ) |
| 64 | | elfzelz 13564 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁)) → 𝑏 ∈ ℤ) |
| 65 | 64 | zred 12722 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁)) → 𝑏 ∈ ℝ) |
| 66 | 65 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) → 𝑏 ∈ ℝ) |
| 67 | | lttri2 11343 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 ≠ 𝑏 ↔ (𝑎 < 𝑏 ∨ 𝑏 < 𝑎))) |
| 68 | 63, 66, 67 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) → (𝑎 ≠ 𝑏 ↔ (𝑎 < 𝑏 ∨ 𝑏 < 𝑎))) |
| 69 | 59, 68 | bitrd 279 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) → (¬ 𝑎 = 𝑏 ↔ (𝑎 < 𝑏 ∨ 𝑏 < 𝑎))) |
| 70 | 69 | imbi1d 341 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) → ((¬ 𝑎 = 𝑏 → (𝐿‘(𝑁↑𝑎)) ≠ (𝐿‘(𝑁↑𝑏))) ↔ ((𝑎 < 𝑏 ∨ 𝑏 < 𝑎) → (𝐿‘(𝑁↑𝑎)) ≠ (𝐿‘(𝑁↑𝑏))))) |
| 71 | 57, 70 | mpbird 257 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) → (¬ 𝑎 = 𝑏 → (𝐿‘(𝑁↑𝑎)) ≠ (𝐿‘(𝑁↑𝑏)))) |
| 72 | 71 | imp 406 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ ¬ 𝑎 = 𝑏) → (𝐿‘(𝑁↑𝑎)) ≠ (𝐿‘(𝑁↑𝑏))) |
| 73 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ ¬ 𝑎 = 𝑏) → (𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥))) = (𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥)))) |
| 74 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑥 = 𝑎) → 𝑥 = 𝑎) |
| 75 | 74 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑥 = 𝑎) → (𝑁↑𝑥) = (𝑁↑𝑎)) |
| 76 | 75 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑥 = 𝑎) → (𝐿‘(𝑁↑𝑥)) = (𝐿‘(𝑁↑𝑎))) |
| 77 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ ¬ 𝑎 = 𝑏) → 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) |
| 78 | | fvexd 6921 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ ¬ 𝑎 = 𝑏) → (𝐿‘(𝑁↑𝑎)) ∈ V) |
| 79 | 73, 76, 77, 78 | fvmptd 7023 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ ¬ 𝑎 = 𝑏) → ((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥)))‘𝑎) = (𝐿‘(𝑁↑𝑎))) |
| 80 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑥 = 𝑏) → 𝑥 = 𝑏) |
| 81 | 80 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑥 = 𝑏) → (𝑁↑𝑥) = (𝑁↑𝑏)) |
| 82 | 81 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑥 = 𝑏) → (𝐿‘(𝑁↑𝑥)) = (𝐿‘(𝑁↑𝑏))) |
| 83 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ ¬ 𝑎 = 𝑏) → 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) |
| 84 | | fvexd 6921 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ ¬ 𝑎 = 𝑏) → (𝐿‘(𝑁↑𝑏)) ∈ V) |
| 85 | 73, 82, 83, 84 | fvmptd 7023 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ ¬ 𝑎 = 𝑏) → ((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥)))‘𝑏) = (𝐿‘(𝑁↑𝑏))) |
| 86 | 79, 85 | neeq12d 3002 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ ¬ 𝑎 = 𝑏) → (((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥)))‘𝑎) ≠ ((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥)))‘𝑏) ↔ (𝐿‘(𝑁↑𝑎)) ≠ (𝐿‘(𝑁↑𝑏)))) |
| 87 | 72, 86 | mpbird 257 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ ¬ 𝑎 = 𝑏) → ((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥)))‘𝑎) ≠ ((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥)))‘𝑏)) |
| 88 | 87 | neneqd 2945 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ ¬ 𝑎 = 𝑏) → ¬ ((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥)))‘𝑎) = ((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥)))‘𝑏)) |
| 89 | 88 | ex 412 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) → (¬ 𝑎 = 𝑏 → ¬ ((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥)))‘𝑎) = ((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥)))‘𝑏))) |
| 90 | 89 | con4d 115 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) ∧ 𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))) → (((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥)))‘𝑎) = ((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥)))‘𝑏) → 𝑎 = 𝑏)) |
| 91 | 90 | ralrimiva 3146 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))) → ∀𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))(((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥)))‘𝑎) = ((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥)))‘𝑏) → 𝑎 = 𝑏)) |
| 92 | 91 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))∀𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))(((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥)))‘𝑎) = ((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥)))‘𝑏) → 𝑎 = 𝑏)) |
| 93 | 40, 92 | jca 511 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥))):(1...((odℤ‘𝑅)‘𝑁))⟶(𝐿 “ 𝐸) ∧ ∀𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))∀𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))(((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥)))‘𝑎) = ((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥)))‘𝑏) → 𝑎 = 𝑏))) |
| 94 | | dff13 7275 |
. . . 4
⊢ ((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥))):(1...((odℤ‘𝑅)‘𝑁))–1-1→(𝐿 “ 𝐸) ↔ ((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥))):(1...((odℤ‘𝑅)‘𝑁))⟶(𝐿 “ 𝐸) ∧ ∀𝑎 ∈
(1...((odℤ‘𝑅)‘𝑁))∀𝑏 ∈
(1...((odℤ‘𝑅)‘𝑁))(((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥)))‘𝑎) = ((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥)))‘𝑏) → 𝑎 = 𝑏))) |
| 95 | 93, 94 | sylibr 234 |
. . 3
⊢ (𝜑 → (𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥))):(1...((odℤ‘𝑅)‘𝑁))–1-1→(𝐿 “ 𝐸)) |
| 96 | | hashf1dmcdm 14483 |
. . 3
⊢ (((𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥))) ∈ V ∧ (𝐿 “ 𝐸) ∈ V ∧ (𝑥 ∈
(1...((odℤ‘𝑅)‘𝑁)) ↦ (𝐿‘(𝑁↑𝑥))):(1...((odℤ‘𝑅)‘𝑁))–1-1→(𝐿 “ 𝐸)) →
(♯‘(1...((odℤ‘𝑅)‘𝑁))) ≤ (♯‘(𝐿 “ 𝐸))) |
| 97 | 11, 16, 95, 96 | syl3anc 1373 |
. 2
⊢ (𝜑 →
(♯‘(1...((odℤ‘𝑅)‘𝑁))) ≤ (♯‘(𝐿 “ 𝐸))) |
| 98 | 9, 97 | eqbrtrrd 5167 |
1
⊢ (𝜑 →
((odℤ‘𝑅)‘𝑁) ≤ (♯‘(𝐿 “ 𝐸))) |