Step | Hyp | Ref
| Expression |
1 | | reprgt.a |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ (1...𝑁)) |
2 | | fz1ssnn 13275 |
. . . 4
⊢
(1...𝑁) ⊆
ℕ |
3 | 1, 2 | sstrdi 3933 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℕ) |
4 | | reprgt.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
5 | | reprgt.s |
. . 3
⊢ (𝜑 → 𝑆 ∈
ℕ0) |
6 | 3, 4, 5 | reprval 32576 |
. 2
⊢ (𝜑 → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀}) |
7 | | fzofi 13682 |
. . . . . . . 8
⊢
(0..^𝑆) ∈
Fin |
8 | 7 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → (0..^𝑆) ∈ Fin) |
9 | | nnssre 11965 |
. . . . . . . . . . . . 13
⊢ ℕ
⊆ ℝ |
10 | 3, 9 | sstrdi 3933 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
11 | 10 | ralrimivw 3114 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑎 ∈ (0..^𝑆)𝐴 ⊆ ℝ) |
12 | 11 | ralrimivw 3114 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑐 ∈ (𝐴 ↑m (0..^𝑆))∀𝑎 ∈ (0..^𝑆)𝐴 ⊆ ℝ) |
13 | 12 | r19.21bi 3133 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → ∀𝑎 ∈ (0..^𝑆)𝐴 ⊆ ℝ) |
14 | 13 | r19.21bi 3133 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℝ) |
15 | | ovex 7301 |
. . . . . . . . . . . . . 14
⊢
(1...𝑁) ∈
V |
16 | 15 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1...𝑁) ∈ V) |
17 | 16, 1 | ssexd 5247 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ V) |
18 | 17 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝐴 ∈ V) |
19 | 7 | elexi 3449 |
. . . . . . . . . . . 12
⊢
(0..^𝑆) ∈
V |
20 | 19 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → (0..^𝑆) ∈ V) |
21 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) |
22 | | elmapg 8616 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↔ 𝑐:(0..^𝑆)⟶𝐴)) |
23 | 22 | biimpa 477 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑐:(0..^𝑆)⟶𝐴) |
24 | 18, 20, 21, 23 | syl21anc 835 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑐:(0..^𝑆)⟶𝐴) |
25 | 24 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑐:(0..^𝑆)⟶𝐴) |
26 | | simpr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆)) |
27 | 25, 26 | ffvelrnd 6955 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ 𝐴) |
28 | 14, 27 | sseldd 3922 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ ℝ) |
29 | 8, 28 | fsumrecl 15434 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ∈ ℝ) |
30 | 5 | nn0red 12282 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ ℝ) |
31 | 30 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑆 ∈ ℝ) |
32 | | reprgt.n |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
33 | 32 | nn0red 12282 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℝ) |
34 | 33 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑁 ∈ ℝ) |
35 | 31, 34 | remulcld 10993 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → (𝑆 · 𝑁) ∈ ℝ) |
36 | 4 | zred 12414 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℝ) |
37 | 36 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑀 ∈ ℝ) |
38 | 33 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑁 ∈ ℝ) |
39 | 1 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ (1...𝑁)) |
40 | 39, 27 | sseldd 3922 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ (1...𝑁)) |
41 | | elfzle2 13248 |
. . . . . . . . . 10
⊢ ((𝑐‘𝑎) ∈ (1...𝑁) → (𝑐‘𝑎) ≤ 𝑁) |
42 | 40, 41 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ≤ 𝑁) |
43 | 8, 28, 38, 42 | fsumle 15499 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ≤ Σ𝑎 ∈ (0..^𝑆)𝑁) |
44 | 33 | recnd 10991 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℂ) |
45 | | fsumconst 15490 |
. . . . . . . . . . 11
⊢
(((0..^𝑆) ∈ Fin
∧ 𝑁 ∈ ℂ)
→ Σ𝑎 ∈
(0..^𝑆)𝑁 = ((♯‘(0..^𝑆)) · 𝑁)) |
46 | 7, 44, 45 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑎 ∈ (0..^𝑆)𝑁 = ((♯‘(0..^𝑆)) · 𝑁)) |
47 | | hashfzo0 14133 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ ℕ0
→ (♯‘(0..^𝑆)) = 𝑆) |
48 | 5, 47 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘(0..^𝑆)) = 𝑆) |
49 | 48 | oveq1d 7283 |
. . . . . . . . . 10
⊢ (𝜑 → ((♯‘(0..^𝑆)) · 𝑁) = (𝑆 · 𝑁)) |
50 | 46, 49 | eqtrd 2778 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑎 ∈ (0..^𝑆)𝑁 = (𝑆 · 𝑁)) |
51 | 50 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → Σ𝑎 ∈ (0..^𝑆)𝑁 = (𝑆 · 𝑁)) |
52 | 43, 51 | breqtrd 5100 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ≤ (𝑆 · 𝑁)) |
53 | | reprgt.1 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 · 𝑁) < 𝑀) |
54 | 53 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → (𝑆 · 𝑁) < 𝑀) |
55 | 29, 35, 37, 52, 54 | lelttrd 11121 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) < 𝑀) |
56 | 29, 55 | ltned 11099 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ≠ 𝑀) |
57 | 56 | neneqd 2948 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → ¬ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀) |
58 | 57 | ralrimiva 3113 |
. . 3
⊢ (𝜑 → ∀𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ¬ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀) |
59 | | rabeq0 4319 |
. . 3
⊢ ({𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀} = ∅ ↔ ∀𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ¬ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀) |
60 | 58, 59 | sylibr 233 |
. 2
⊢ (𝜑 → {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀} = ∅) |
61 | 6, 60 | eqtrd 2778 |
1
⊢ (𝜑 → (𝐴(repr‘𝑆)𝑀) = ∅) |