Step | Hyp | Ref
| Expression |
1 | | reprval.a |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℕ) |
2 | | reprval.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
3 | | reprval.s |
. . 3
⊢ (𝜑 → 𝑆 ∈
ℕ0) |
4 | 1, 2, 3 | reprval 30688 |
. 2
⊢ (𝜑 → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀}) |
5 | 2 | zred 11482 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℝ) |
6 | 5 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) → 𝑀 ∈ ℝ) |
7 | 3 | nn0red 11352 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ ℝ) |
8 | 7 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) → 𝑆 ∈ ℝ) |
9 | | fzofi 12773 |
. . . . . . . . . 10
⊢
(0..^𝑆) ∈
Fin |
10 | 9 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) → (0..^𝑆) ∈ Fin) |
11 | | nnssre 11024 |
. . . . . . . . . . . . 13
⊢ ℕ
⊆ ℝ |
12 | 11 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℕ ⊆
ℝ) |
13 | 1, 12 | sstrd 3613 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
14 | 13 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℝ) |
15 | | nnex 11026 |
. . . . . . . . . . . . . . . 16
⊢ ℕ
∈ V |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ℕ ∈
V) |
17 | 16, 1 | ssexd 4805 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ V) |
18 | 17 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) → 𝐴 ∈ V) |
19 | 9 | elexi 3213 |
. . . . . . . . . . . . . 14
⊢
(0..^𝑆) ∈
V |
20 | 19 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) → (0..^𝑆) ∈ V) |
21 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) → 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) |
22 | | elmapg 7870 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → (𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆)) ↔ 𝑐:(0..^𝑆)⟶𝐴)) |
23 | 22 | biimpa 501 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) → 𝑐:(0..^𝑆)⟶𝐴) |
24 | 18, 20, 21, 23 | syl21anc 1325 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) → 𝑐:(0..^𝑆)⟶𝐴) |
25 | 24 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑐:(0..^𝑆)⟶𝐴) |
26 | | simpr 477 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆)) |
27 | 25, 26 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ 𝐴) |
28 | 14, 27 | sseldd 3604 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ ℝ) |
29 | 10, 28 | fsumrecl 14465 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ∈ ℝ) |
30 | | reprlt.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 < 𝑆) |
31 | 30 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) → 𝑀 < 𝑆) |
32 | | ax-1cn 9994 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
33 | | fsumconst 14522 |
. . . . . . . . . . . . 13
⊢
(((0..^𝑆) ∈ Fin
∧ 1 ∈ ℂ) → Σ𝑎 ∈ (0..^𝑆)1 = ((#‘(0..^𝑆)) · 1)) |
34 | 9, 32, 33 | mp2an 708 |
. . . . . . . . . . . 12
⊢
Σ𝑎 ∈
(0..^𝑆)1 =
((#‘(0..^𝑆)) ·
1) |
35 | | hashcl 13147 |
. . . . . . . . . . . . . . 15
⊢
((0..^𝑆) ∈ Fin
→ (#‘(0..^𝑆))
∈ ℕ0) |
36 | 9, 35 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(#‘(0..^𝑆))
∈ ℕ0 |
37 | 36 | nn0cni 11304 |
. . . . . . . . . . . . 13
⊢
(#‘(0..^𝑆))
∈ ℂ |
38 | 37 | mulid1i 10042 |
. . . . . . . . . . . 12
⊢
((#‘(0..^𝑆))
· 1) = (#‘(0..^𝑆)) |
39 | 34, 38 | eqtri 2644 |
. . . . . . . . . . 11
⊢
Σ𝑎 ∈
(0..^𝑆)1 =
(#‘(0..^𝑆)) |
40 | | hashfzo0 13217 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ ℕ0
→ (#‘(0..^𝑆)) =
𝑆) |
41 | 3, 40 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘(0..^𝑆)) = 𝑆) |
42 | 39, 41 | syl5eq 2668 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑎 ∈ (0..^𝑆)1 = 𝑆) |
43 | 42 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) → Σ𝑎 ∈ (0..^𝑆)1 = 𝑆) |
44 | | 1red 10055 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 1 ∈ ℝ) |
45 | 1 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℕ) |
46 | 45, 27 | sseldd 3604 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ ℕ) |
47 | | nnge1 11046 |
. . . . . . . . . . 11
⊢ ((𝑐‘𝑎) ∈ ℕ → 1 ≤ (𝑐‘𝑎)) |
48 | 46, 47 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) ∧ 𝑎 ∈ (0..^𝑆)) → 1 ≤ (𝑐‘𝑎)) |
49 | 10, 44, 28, 48 | fsumle 14531 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) → Σ𝑎 ∈ (0..^𝑆)1 ≤ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎)) |
50 | 43, 49 | eqbrtrrd 4677 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) → 𝑆 ≤ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎)) |
51 | 6, 8, 29, 31, 50 | ltletrd 10197 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) → 𝑀 < Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎)) |
52 | 6, 51 | ltned 10173 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) → 𝑀 ≠ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎)) |
53 | 52 | necomd 2849 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ≠ 𝑀) |
54 | 53 | neneqd 2799 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆))) → ¬ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀) |
55 | 54 | ralrimiva 2966 |
. . 3
⊢ (𝜑 → ∀𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆)) ¬ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀) |
56 | | rabeq0 3957 |
. . 3
⊢ ({𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀} = ∅ ↔ ∀𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆)) ¬ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀) |
57 | 55, 56 | sylibr 224 |
. 2
⊢ (𝜑 → {𝑐 ∈ (𝐴 ↑𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀} = ∅) |
58 | 4, 57 | eqtrd 2656 |
1
⊢ (𝜑 → (𝐴(repr‘𝑆)𝑀) = ∅) |