| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | reprval.a | . . 3
⊢ (𝜑 → 𝐴 ⊆ ℕ) | 
| 2 |  | reprval.m | . . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 3 |  | reprval.s | . . 3
⊢ (𝜑 → 𝑆 ∈
ℕ0) | 
| 4 | 1, 2, 3 | reprval 34625 | . 2
⊢ (𝜑 → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀}) | 
| 5 | 2 | zred 12722 | . . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 6 | 5 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑀 ∈ ℝ) | 
| 7 | 3 | nn0red 12588 | . . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ ℝ) | 
| 8 | 7 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑆 ∈ ℝ) | 
| 9 |  | fzofi 14015 | . . . . . . . . . 10
⊢
(0..^𝑆) ∈
Fin | 
| 10 | 9 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → (0..^𝑆) ∈ Fin) | 
| 11 |  | nnssre 12270 | . . . . . . . . . . . . 13
⊢ ℕ
⊆ ℝ | 
| 12 | 11 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → ℕ ⊆
ℝ) | 
| 13 | 1, 12 | sstrd 3994 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ ℝ) | 
| 14 | 13 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℝ) | 
| 15 |  | nnex 12272 | . . . . . . . . . . . . . . . 16
⊢ ℕ
∈ V | 
| 16 | 15 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ℕ ∈
V) | 
| 17 | 16, 1 | ssexd 5324 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ V) | 
| 18 | 17 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝐴 ∈ V) | 
| 19 | 9 | elexi 3503 | . . . . . . . . . . . . . 14
⊢
(0..^𝑆) ∈
V | 
| 20 | 19 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → (0..^𝑆) ∈ V) | 
| 21 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) | 
| 22 |  | elmapg 8879 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↔ 𝑐:(0..^𝑆)⟶𝐴)) | 
| 23 | 22 | biimpa 476 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑐:(0..^𝑆)⟶𝐴) | 
| 24 | 18, 20, 21, 23 | syl21anc 838 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑐:(0..^𝑆)⟶𝐴) | 
| 25 | 24 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑐:(0..^𝑆)⟶𝐴) | 
| 26 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆)) | 
| 27 | 25, 26 | ffvelcdmd 7105 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ 𝐴) | 
| 28 | 14, 27 | sseldd 3984 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ ℝ) | 
| 29 | 10, 28 | fsumrecl 15770 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ∈ ℝ) | 
| 30 |  | reprlt.1 | . . . . . . . . 9
⊢ (𝜑 → 𝑀 < 𝑆) | 
| 31 | 30 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑀 < 𝑆) | 
| 32 |  | ax-1cn 11213 | . . . . . . . . . . . . 13
⊢ 1 ∈
ℂ | 
| 33 |  | fsumconst 15826 | . . . . . . . . . . . . 13
⊢
(((0..^𝑆) ∈ Fin
∧ 1 ∈ ℂ) → Σ𝑎 ∈ (0..^𝑆)1 = ((♯‘(0..^𝑆)) · 1)) | 
| 34 | 9, 32, 33 | mp2an 692 | . . . . . . . . . . . 12
⊢
Σ𝑎 ∈
(0..^𝑆)1 =
((♯‘(0..^𝑆))
· 1) | 
| 35 |  | hashcl 14395 | . . . . . . . . . . . . . . 15
⊢
((0..^𝑆) ∈ Fin
→ (♯‘(0..^𝑆)) ∈
ℕ0) | 
| 36 | 9, 35 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢
(♯‘(0..^𝑆)) ∈
ℕ0 | 
| 37 | 36 | nn0cni 12538 | . . . . . . . . . . . . 13
⊢
(♯‘(0..^𝑆)) ∈ ℂ | 
| 38 | 37 | mulridi 11265 | . . . . . . . . . . . 12
⊢
((♯‘(0..^𝑆)) · 1) = (♯‘(0..^𝑆)) | 
| 39 | 34, 38 | eqtri 2765 | . . . . . . . . . . 11
⊢
Σ𝑎 ∈
(0..^𝑆)1 =
(♯‘(0..^𝑆)) | 
| 40 |  | hashfzo0 14469 | . . . . . . . . . . . 12
⊢ (𝑆 ∈ ℕ0
→ (♯‘(0..^𝑆)) = 𝑆) | 
| 41 | 3, 40 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (♯‘(0..^𝑆)) = 𝑆) | 
| 42 | 39, 41 | eqtrid 2789 | . . . . . . . . . 10
⊢ (𝜑 → Σ𝑎 ∈ (0..^𝑆)1 = 𝑆) | 
| 43 | 42 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → Σ𝑎 ∈ (0..^𝑆)1 = 𝑆) | 
| 44 |  | 1red 11262 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 1 ∈ ℝ) | 
| 45 | 1 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℕ) | 
| 46 | 45, 27 | sseldd 3984 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ ℕ) | 
| 47 |  | nnge1 12294 | . . . . . . . . . . 11
⊢ ((𝑐‘𝑎) ∈ ℕ → 1 ≤ (𝑐‘𝑎)) | 
| 48 | 46, 47 | syl 17 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 1 ≤ (𝑐‘𝑎)) | 
| 49 | 10, 44, 28, 48 | fsumle 15835 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → Σ𝑎 ∈ (0..^𝑆)1 ≤ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎)) | 
| 50 | 43, 49 | eqbrtrrd 5167 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑆 ≤ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎)) | 
| 51 | 6, 8, 29, 31, 50 | ltletrd 11421 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑀 < Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎)) | 
| 52 | 6, 51 | ltned 11397 | . . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑀 ≠ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎)) | 
| 53 | 52 | necomd 2996 | . . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ≠ 𝑀) | 
| 54 | 53 | neneqd 2945 | . . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → ¬ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀) | 
| 55 | 54 | ralrimiva 3146 | . . 3
⊢ (𝜑 → ∀𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ¬ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀) | 
| 56 |  | rabeq0 4388 | . . 3
⊢ ({𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀} = ∅ ↔ ∀𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ¬ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀) | 
| 57 | 55, 56 | sylibr 234 | . 2
⊢ (𝜑 → {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀} = ∅) | 
| 58 | 4, 57 | eqtrd 2777 | 1
⊢ (𝜑 → (𝐴(repr‘𝑆)𝑀) = ∅) |