| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | reprgt.a | . . . 4
⊢ (𝜑 → 𝐴 ⊆ (1...𝑁)) | 
| 2 |  | fz1ssnn 13596 | . . . 4
⊢
(1...𝑁) ⊆
ℕ | 
| 3 | 1, 2 | sstrdi 3995 | . . 3
⊢ (𝜑 → 𝐴 ⊆ ℕ) | 
| 4 |  | reprgt.m | . . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 5 |  | reprgt.s | . . 3
⊢ (𝜑 → 𝑆 ∈
ℕ0) | 
| 6 | 3, 4, 5 | reprval 34626 | . 2
⊢ (𝜑 → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀}) | 
| 7 |  | fzofi 14016 | . . . . . . . 8
⊢
(0..^𝑆) ∈
Fin | 
| 8 | 7 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → (0..^𝑆) ∈ Fin) | 
| 9 |  | nnssre 12271 | . . . . . . . . . . . . 13
⊢ ℕ
⊆ ℝ | 
| 10 | 3, 9 | sstrdi 3995 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ⊆ ℝ) | 
| 11 | 10 | ralrimivw 3149 | . . . . . . . . . . 11
⊢ (𝜑 → ∀𝑎 ∈ (0..^𝑆)𝐴 ⊆ ℝ) | 
| 12 | 11 | ralrimivw 3149 | . . . . . . . . . 10
⊢ (𝜑 → ∀𝑐 ∈ (𝐴 ↑m (0..^𝑆))∀𝑎 ∈ (0..^𝑆)𝐴 ⊆ ℝ) | 
| 13 | 12 | r19.21bi 3250 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → ∀𝑎 ∈ (0..^𝑆)𝐴 ⊆ ℝ) | 
| 14 | 13 | r19.21bi 3250 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℝ) | 
| 15 |  | ovex 7465 | . . . . . . . . . . . . . 14
⊢
(1...𝑁) ∈
V | 
| 16 | 15 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → (1...𝑁) ∈ V) | 
| 17 | 16, 1 | ssexd 5323 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ V) | 
| 18 | 17 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝐴 ∈ V) | 
| 19 | 7 | elexi 3502 | . . . . . . . . . . . 12
⊢
(0..^𝑆) ∈
V | 
| 20 | 19 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → (0..^𝑆) ∈ V) | 
| 21 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) | 
| 22 |  | elmapg 8880 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↔ 𝑐:(0..^𝑆)⟶𝐴)) | 
| 23 | 22 | biimpa 476 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑐:(0..^𝑆)⟶𝐴) | 
| 24 | 18, 20, 21, 23 | syl21anc 837 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑐:(0..^𝑆)⟶𝐴) | 
| 25 | 24 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑐:(0..^𝑆)⟶𝐴) | 
| 26 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆)) | 
| 27 | 25, 26 | ffvelcdmd 7104 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ 𝐴) | 
| 28 | 14, 27 | sseldd 3983 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ ℝ) | 
| 29 | 8, 28 | fsumrecl 15771 | . . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ∈ ℝ) | 
| 30 | 5 | nn0red 12590 | . . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ ℝ) | 
| 31 | 30 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑆 ∈ ℝ) | 
| 32 |  | reprgt.n | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 33 | 32 | nn0red 12590 | . . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 34 | 33 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑁 ∈ ℝ) | 
| 35 | 31, 34 | remulcld 11292 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → (𝑆 · 𝑁) ∈ ℝ) | 
| 36 | 4 | zred 12724 | . . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 37 | 36 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑀 ∈ ℝ) | 
| 38 | 33 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑁 ∈ ℝ) | 
| 39 | 1 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ (1...𝑁)) | 
| 40 | 39, 27 | sseldd 3983 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ (1...𝑁)) | 
| 41 |  | elfzle2 13569 | . . . . . . . . . 10
⊢ ((𝑐‘𝑎) ∈ (1...𝑁) → (𝑐‘𝑎) ≤ 𝑁) | 
| 42 | 40, 41 | syl 17 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ≤ 𝑁) | 
| 43 | 8, 28, 38, 42 | fsumle 15836 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ≤ Σ𝑎 ∈ (0..^𝑆)𝑁) | 
| 44 | 33 | recnd 11290 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 45 |  | fsumconst 15827 | . . . . . . . . . . 11
⊢
(((0..^𝑆) ∈ Fin
∧ 𝑁 ∈ ℂ)
→ Σ𝑎 ∈
(0..^𝑆)𝑁 = ((♯‘(0..^𝑆)) · 𝑁)) | 
| 46 | 7, 44, 45 | sylancr 587 | . . . . . . . . . 10
⊢ (𝜑 → Σ𝑎 ∈ (0..^𝑆)𝑁 = ((♯‘(0..^𝑆)) · 𝑁)) | 
| 47 |  | hashfzo0 14470 | . . . . . . . . . . . 12
⊢ (𝑆 ∈ ℕ0
→ (♯‘(0..^𝑆)) = 𝑆) | 
| 48 | 5, 47 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (♯‘(0..^𝑆)) = 𝑆) | 
| 49 | 48 | oveq1d 7447 | . . . . . . . . . 10
⊢ (𝜑 → ((♯‘(0..^𝑆)) · 𝑁) = (𝑆 · 𝑁)) | 
| 50 | 46, 49 | eqtrd 2776 | . . . . . . . . 9
⊢ (𝜑 → Σ𝑎 ∈ (0..^𝑆)𝑁 = (𝑆 · 𝑁)) | 
| 51 | 50 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → Σ𝑎 ∈ (0..^𝑆)𝑁 = (𝑆 · 𝑁)) | 
| 52 | 43, 51 | breqtrd 5168 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ≤ (𝑆 · 𝑁)) | 
| 53 |  | reprgt.1 | . . . . . . . 8
⊢ (𝜑 → (𝑆 · 𝑁) < 𝑀) | 
| 54 | 53 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → (𝑆 · 𝑁) < 𝑀) | 
| 55 | 29, 35, 37, 52, 54 | lelttrd 11420 | . . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) < 𝑀) | 
| 56 | 29, 55 | ltned 11398 | . . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ≠ 𝑀) | 
| 57 | 56 | neneqd 2944 | . . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → ¬ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀) | 
| 58 | 57 | ralrimiva 3145 | . . 3
⊢ (𝜑 → ∀𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ¬ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀) | 
| 59 |  | rabeq0 4387 | . . 3
⊢ ({𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀} = ∅ ↔ ∀𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ¬ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀) | 
| 60 | 58, 59 | sylibr 234 | . 2
⊢ (𝜑 → {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀} = ∅) | 
| 61 | 6, 60 | eqtrd 2776 | 1
⊢ (𝜑 → (𝐴(repr‘𝑆)𝑀) = ∅) |