Step |
Hyp |
Ref |
Expression |
1 |
|
reprval.a |
⊢ ( 𝜑 → 𝐴 ⊆ ℕ ) |
2 |
|
reprval.m |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
3 |
|
reprval.s |
⊢ ( 𝜑 → 𝑆 ∈ ℕ0 ) |
4 |
|
reprlt.1 |
⊢ ( 𝜑 → 𝑀 < 𝑆 ) |
5 |
1 2 3
|
reprval |
⊢ ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) = { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } ) |
6 |
2
|
zred |
⊢ ( 𝜑 → 𝑀 ∈ ℝ ) |
7 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → 𝑀 ∈ ℝ ) |
8 |
3
|
nn0red |
⊢ ( 𝜑 → 𝑆 ∈ ℝ ) |
9 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → 𝑆 ∈ ℝ ) |
10 |
|
fzofi |
⊢ ( 0 ..^ 𝑆 ) ∈ Fin |
11 |
10
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → ( 0 ..^ 𝑆 ) ∈ Fin ) |
12 |
|
nnssre |
⊢ ℕ ⊆ ℝ |
13 |
12
|
a1i |
⊢ ( 𝜑 → ℕ ⊆ ℝ ) |
14 |
1 13
|
sstrd |
⊢ ( 𝜑 → 𝐴 ⊆ ℝ ) |
15 |
14
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝐴 ⊆ ℝ ) |
16 |
|
nnex |
⊢ ℕ ∈ V |
17 |
16
|
a1i |
⊢ ( 𝜑 → ℕ ∈ V ) |
18 |
17 1
|
ssexd |
⊢ ( 𝜑 → 𝐴 ∈ V ) |
19 |
18
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → 𝐴 ∈ V ) |
20 |
10
|
elexi |
⊢ ( 0 ..^ 𝑆 ) ∈ V |
21 |
20
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → ( 0 ..^ 𝑆 ) ∈ V ) |
22 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) |
23 |
|
elmapg |
⊢ ( ( 𝐴 ∈ V ∧ ( 0 ..^ 𝑆 ) ∈ V ) → ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↔ 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ) ) |
24 |
23
|
biimpa |
⊢ ( ( ( 𝐴 ∈ V ∧ ( 0 ..^ 𝑆 ) ∈ V ) ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ) |
25 |
19 21 22 24
|
syl21anc |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ) |
26 |
25
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ) |
27 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑎 ∈ ( 0 ..^ 𝑆 ) ) |
28 |
26 27
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐 ‘ 𝑎 ) ∈ 𝐴 ) |
29 |
15 28
|
sseldd |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐 ‘ 𝑎 ) ∈ ℝ ) |
30 |
11 29
|
fsumrecl |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) ∈ ℝ ) |
31 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → 𝑀 < 𝑆 ) |
32 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
33 |
|
fsumconst |
⊢ ( ( ( 0 ..^ 𝑆 ) ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) 1 = ( ( ♯ ‘ ( 0 ..^ 𝑆 ) ) · 1 ) ) |
34 |
10 32 33
|
mp2an |
⊢ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) 1 = ( ( ♯ ‘ ( 0 ..^ 𝑆 ) ) · 1 ) |
35 |
|
hashcl |
⊢ ( ( 0 ..^ 𝑆 ) ∈ Fin → ( ♯ ‘ ( 0 ..^ 𝑆 ) ) ∈ ℕ0 ) |
36 |
10 35
|
ax-mp |
⊢ ( ♯ ‘ ( 0 ..^ 𝑆 ) ) ∈ ℕ0 |
37 |
36
|
nn0cni |
⊢ ( ♯ ‘ ( 0 ..^ 𝑆 ) ) ∈ ℂ |
38 |
37
|
mulid1i |
⊢ ( ( ♯ ‘ ( 0 ..^ 𝑆 ) ) · 1 ) = ( ♯ ‘ ( 0 ..^ 𝑆 ) ) |
39 |
34 38
|
eqtri |
⊢ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) 1 = ( ♯ ‘ ( 0 ..^ 𝑆 ) ) |
40 |
|
hashfzo0 |
⊢ ( 𝑆 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝑆 ) ) = 𝑆 ) |
41 |
3 40
|
syl |
⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ 𝑆 ) ) = 𝑆 ) |
42 |
39 41
|
syl5eq |
⊢ ( 𝜑 → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) 1 = 𝑆 ) |
43 |
42
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) 1 = 𝑆 ) |
44 |
|
1red |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 1 ∈ ℝ ) |
45 |
1
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝐴 ⊆ ℕ ) |
46 |
45 28
|
sseldd |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐 ‘ 𝑎 ) ∈ ℕ ) |
47 |
|
nnge1 |
⊢ ( ( 𝑐 ‘ 𝑎 ) ∈ ℕ → 1 ≤ ( 𝑐 ‘ 𝑎 ) ) |
48 |
46 47
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 1 ≤ ( 𝑐 ‘ 𝑎 ) ) |
49 |
11 44 29 48
|
fsumle |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) 1 ≤ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) ) |
50 |
43 49
|
eqbrtrrd |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → 𝑆 ≤ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) ) |
51 |
7 9 30 31 50
|
ltletrd |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → 𝑀 < Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) ) |
52 |
7 51
|
ltned |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → 𝑀 ≠ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) ) |
53 |
52
|
necomd |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) ≠ 𝑀 ) |
54 |
53
|
neneqd |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → ¬ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ) |
55 |
54
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ¬ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ) |
56 |
|
rabeq0 |
⊢ ( { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } = ∅ ↔ ∀ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ¬ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ) |
57 |
55 56
|
sylibr |
⊢ ( 𝜑 → { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } = ∅ ) |
58 |
5 57
|
eqtrd |
⊢ ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) = ∅ ) |