| Step | Hyp | Ref
| Expression |
| 1 | | fzofi 14015 |
. . . 4
⊢ (0..^3)
∈ Fin |
| 2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → (0..^3) ∈
Fin) |
| 3 | | hgt750leme.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 4 | 3 | nnnn0d 12587 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 5 | | 3nn0 12544 |
. . . . . . 7
⊢ 3 ∈
ℕ0 |
| 6 | 5 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 3 ∈
ℕ0) |
| 7 | | ssidd 4007 |
. . . . . 6
⊢ (𝜑 → ℕ ⊆
ℕ) |
| 8 | 4, 6, 7 | reprfi2 34638 |
. . . . 5
⊢ (𝜑 →
(ℕ(repr‘3)𝑁)
∈ Fin) |
| 9 | | ssrab2 4080 |
. . . . . 6
⊢ {𝑐 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ⊆
(ℕ(repr‘3)𝑁) |
| 10 | 9 | a1i 11 |
. . . . 5
⊢ (𝜑 → {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ⊆
(ℕ(repr‘3)𝑁)) |
| 11 | 8, 10 | ssfid 9301 |
. . . 4
⊢ (𝜑 → {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ∈
Fin) |
| 12 | 11 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^3)) → {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ∈
Fin) |
| 13 | | vmaf 27162 |
. . . . . 6
⊢
Λ:ℕ⟶ℝ |
| 14 | 13 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) →
Λ:ℕ⟶ℝ) |
| 15 | | ssidd 4007 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → ℕ ⊆
ℕ) |
| 16 | 4 | nn0zd 12639 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 17 | 16 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 𝑁 ∈ ℤ) |
| 18 | 5 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 3 ∈
ℕ0) |
| 19 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) |
| 20 | 9, 19 | sselid 3981 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 𝑛 ∈ (ℕ(repr‘3)𝑁)) |
| 21 | 15, 17, 18, 20 | reprf 34627 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 𝑛:(0..^3)⟶ℕ) |
| 22 | | c0ex 11255 |
. . . . . . . . 9
⊢ 0 ∈
V |
| 23 | 22 | tpid1 4768 |
. . . . . . . 8
⊢ 0 ∈
{0, 1, 2} |
| 24 | | fzo0to3tp 13791 |
. . . . . . . 8
⊢ (0..^3) =
{0, 1, 2} |
| 25 | 23, 24 | eleqtrri 2840 |
. . . . . . 7
⊢ 0 ∈
(0..^3) |
| 26 | 25 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 0 ∈
(0..^3)) |
| 27 | 21, 26 | ffvelcdmd 7105 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘0) ∈ ℕ) |
| 28 | 14, 27 | ffvelcdmd 7105 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) →
(Λ‘(𝑛‘0)) ∈ ℝ) |
| 29 | | 1ex 11257 |
. . . . . . . . . 10
⊢ 1 ∈
V |
| 30 | 29 | tpid2 4770 |
. . . . . . . . 9
⊢ 1 ∈
{0, 1, 2} |
| 31 | 30, 24 | eleqtrri 2840 |
. . . . . . . 8
⊢ 1 ∈
(0..^3) |
| 32 | 31 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 1 ∈
(0..^3)) |
| 33 | 21, 32 | ffvelcdmd 7105 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘1) ∈ ℕ) |
| 34 | 14, 33 | ffvelcdmd 7105 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) →
(Λ‘(𝑛‘1)) ∈ ℝ) |
| 35 | | 2ex 12343 |
. . . . . . . . . 10
⊢ 2 ∈
V |
| 36 | 35 | tpid3 4773 |
. . . . . . . . 9
⊢ 2 ∈
{0, 1, 2} |
| 37 | 36, 24 | eleqtrri 2840 |
. . . . . . . 8
⊢ 2 ∈
(0..^3) |
| 38 | 37 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 2 ∈
(0..^3)) |
| 39 | 21, 38 | ffvelcdmd 7105 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘2) ∈ ℕ) |
| 40 | 14, 39 | ffvelcdmd 7105 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) →
(Λ‘(𝑛‘2)) ∈ ℝ) |
| 41 | 34, 40 | remulcld 11291 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) →
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈
ℝ) |
| 42 | 28, 41 | remulcld 11291 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) →
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) ∈ ℝ) |
| 43 | | vmage0 27164 |
. . . . 5
⊢ ((𝑛‘0) ∈ ℕ →
0 ≤ (Λ‘(𝑛‘0))) |
| 44 | 27, 43 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 0 ≤
(Λ‘(𝑛‘0))) |
| 45 | | vmage0 27164 |
. . . . . 6
⊢ ((𝑛‘1) ∈ ℕ →
0 ≤ (Λ‘(𝑛‘1))) |
| 46 | 33, 45 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 0 ≤
(Λ‘(𝑛‘1))) |
| 47 | | vmage0 27164 |
. . . . . 6
⊢ ((𝑛‘2) ∈ ℕ →
0 ≤ (Λ‘(𝑛‘2))) |
| 48 | 39, 47 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 0 ≤
(Λ‘(𝑛‘2))) |
| 49 | 34, 40, 46, 48 | mulge0d 11840 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 0 ≤
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) |
| 50 | 28, 41, 44, 49 | mulge0d 11840 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 0 ≤
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))))) |
| 51 | 2, 12, 42, 50 | fsumiunle 32831 |
. 2
⊢ (𝜑 → Σ𝑛 ∈ ∪
𝑎 ∈ (0..^3){𝑐 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) ·
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ Σ𝑎 ∈ (0..^3)Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) ·
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) |
| 52 | | eqid 2737 |
. . . 4
⊢ {𝑐 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} |
| 53 | | inss2 4238 |
. . . . . 6
⊢ (𝑂 ∩ ℙ) ⊆
ℙ |
| 54 | | prmssnn 16713 |
. . . . . 6
⊢ ℙ
⊆ ℕ |
| 55 | 53, 54 | sstri 3993 |
. . . . 5
⊢ (𝑂 ∩ ℙ) ⊆
ℕ |
| 56 | 55 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑂 ∩ ℙ) ⊆
ℕ) |
| 57 | 52, 7, 56, 4, 6 | reprdifc 34642 |
. . 3
⊢ (𝜑 →
((ℕ(repr‘3)𝑁)
∖ ((𝑂 ∩
ℙ)(repr‘3)𝑁)) =
∪ 𝑎 ∈ (0..^3){𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) |
| 58 | 57 | sumeq1d 15736 |
. 2
⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) ·
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) = Σ𝑛 ∈ ∪ 𝑎 ∈ (0..^3){𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) ·
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) |
| 59 | | ssrab2 4080 |
. . . . . . . 8
⊢ {𝑐 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑐‘0)
∈ (𝑂 ∩ ℙ)}
⊆ (ℕ(repr‘3)𝑁) |
| 60 | 59 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)} ⊆
(ℕ(repr‘3)𝑁)) |
| 61 | 8, 60 | ssfid 9301 |
. . . . . 6
⊢ (𝜑 → {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)} ∈
Fin) |
| 62 | 13 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) →
Λ:ℕ⟶ℝ) |
| 63 | | ssidd 4007 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → ℕ
⊆ ℕ) |
| 64 | 16 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑁 ∈
ℤ) |
| 65 | 5 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → 3
∈ ℕ0) |
| 66 | 60 | sselda 3983 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑛 ∈
(ℕ(repr‘3)𝑁)) |
| 67 | 63, 64, 65, 66 | reprf 34627 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑛:(0..^3)⟶ℕ) |
| 68 | 25 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → 0
∈ (0..^3)) |
| 69 | 67, 68 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘0) ∈
ℕ) |
| 70 | 62, 69 | ffvelcdmd 7105 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) →
(Λ‘(𝑛‘0)) ∈ ℝ) |
| 71 | 31 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → 1
∈ (0..^3)) |
| 72 | 67, 71 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘1) ∈
ℕ) |
| 73 | 62, 72 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) →
(Λ‘(𝑛‘1)) ∈ ℝ) |
| 74 | 37 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → 2
∈ (0..^3)) |
| 75 | 67, 74 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘2) ∈
ℕ) |
| 76 | 62, 75 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) →
(Λ‘(𝑛‘2)) ∈ ℝ) |
| 77 | 73, 76 | remulcld 11291 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) →
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈
ℝ) |
| 78 | 70, 77 | remulcld 11291 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) →
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) ∈ ℝ) |
| 79 | 61, 78 | fsumrecl 15770 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) ∈ ℝ) |
| 80 | 79 | recnd 11289 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) ∈ ℂ) |
| 81 | | fsumconst 15826 |
. . . 4
⊢ (((0..^3)
∈ Fin ∧ Σ𝑛
∈ {𝑐 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑐‘0)
∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) ∈ ℂ) →
Σ𝑎 ∈
(0..^3)Σ𝑛 ∈
{𝑐 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑐‘0)
∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) = ((♯‘(0..^3))
· Σ𝑛 ∈
{𝑐 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑐‘0)
∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))))) |
| 82 | 2, 80, 81 | syl2anc 584 |
. . 3
⊢ (𝜑 → Σ𝑎 ∈ (0..^3)Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) = ((♯‘(0..^3))
· Σ𝑛 ∈
{𝑐 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑐‘0)
∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))))) |
| 83 | | fveq1 6905 |
. . . . . . . 8
⊢ (𝑛 = (𝐹‘𝑒) → (𝑛‘0) = ((𝐹‘𝑒)‘0)) |
| 84 | 83 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑛 = (𝐹‘𝑒) → (Λ‘(𝑛‘0)) = (Λ‘((𝐹‘𝑒)‘0))) |
| 85 | | fveq1 6905 |
. . . . . . . . 9
⊢ (𝑛 = (𝐹‘𝑒) → (𝑛‘1) = ((𝐹‘𝑒)‘1)) |
| 86 | 85 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝑛 = (𝐹‘𝑒) → (Λ‘(𝑛‘1)) = (Λ‘((𝐹‘𝑒)‘1))) |
| 87 | | fveq1 6905 |
. . . . . . . . 9
⊢ (𝑛 = (𝐹‘𝑒) → (𝑛‘2) = ((𝐹‘𝑒)‘2)) |
| 88 | 87 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝑛 = (𝐹‘𝑒) → (Λ‘(𝑛‘2)) = (Λ‘((𝐹‘𝑒)‘2))) |
| 89 | 86, 88 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑛 = (𝐹‘𝑒) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) =
((Λ‘((𝐹‘𝑒)‘1)) · (Λ‘((𝐹‘𝑒)‘2)))) |
| 90 | 84, 89 | oveq12d 7449 |
. . . . . 6
⊢ (𝑛 = (𝐹‘𝑒) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) = ((Λ‘((𝐹‘𝑒)‘0)) · ((Λ‘((𝐹‘𝑒)‘1)) · (Λ‘((𝐹‘𝑒)‘2))))) |
| 91 | | 3nn 12345 |
. . . . . . . . . 10
⊢ 3 ∈
ℕ |
| 92 | 91 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 3 ∈
ℕ) |
| 93 | 92 | ralrimivw 3150 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑎 ∈ (0..^3)3 ∈
ℕ) |
| 94 | 93 | r19.21bi 3251 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^3)) → 3 ∈
ℕ) |
| 95 | 16 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^3)) → 𝑁 ∈ ℤ) |
| 96 | | ssidd 4007 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^3)) → ℕ ⊆
ℕ) |
| 97 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^3)) → 𝑎 ∈ (0..^3)) |
| 98 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑑 → (𝑐‘0) = (𝑑‘0)) |
| 99 | 98 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑐 = 𝑑 → ((𝑐‘0) ∈ (𝑂 ∩ ℙ) ↔ (𝑑‘0) ∈ (𝑂 ∩ ℙ))) |
| 100 | 99 | notbid 318 |
. . . . . . . 8
⊢ (𝑐 = 𝑑 → (¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ) ↔ ¬ (𝑑‘0) ∈ (𝑂 ∩
ℙ))) |
| 101 | 100 | cbvrabv 3447 |
. . . . . . 7
⊢ {𝑐 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑐‘0)
∈ (𝑂 ∩ ℙ)} =
{𝑑 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑑‘0)
∈ (𝑂 ∩
ℙ)} |
| 102 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑑 → (𝑐‘𝑎) = (𝑑‘𝑎)) |
| 103 | 102 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑐 = 𝑑 → ((𝑐‘𝑎) ∈ (𝑂 ∩ ℙ) ↔ (𝑑‘𝑎) ∈ (𝑂 ∩ ℙ))) |
| 104 | 103 | notbid 318 |
. . . . . . . 8
⊢ (𝑐 = 𝑑 → (¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ) ↔ ¬ (𝑑‘𝑎) ∈ (𝑂 ∩ ℙ))) |
| 105 | 104 | cbvrabv 3447 |
. . . . . . 7
⊢ {𝑐 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} = {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘𝑎) ∈ (𝑂 ∩ ℙ)} |
| 106 | | eqid 2737 |
. . . . . . 7
⊢ if(𝑎 = 0, ( I ↾ (0..^3)),
((pmTrsp‘(0..^3))‘{𝑎, 0})) = if(𝑎 = 0, ( I ↾ (0..^3)),
((pmTrsp‘(0..^3))‘{𝑎, 0})) |
| 107 | | hgt750lema.f |
. . . . . . 7
⊢ 𝐹 = (𝑑 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ↦ (𝑑 ∘ if(𝑎 = 0, ( I ↾ (0..^3)),
((pmTrsp‘(0..^3))‘{𝑎, 0})))) |
| 108 | 94, 95, 96, 97, 101, 105, 106, 107 | reprpmtf1o 34641 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^3)) → 𝐹:{𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}–1-1-onto→{𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩
ℙ)}) |
| 109 | | eqidd 2738 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑒 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → (𝐹‘𝑒) = (𝐹‘𝑒)) |
| 110 | 78 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) →
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) ∈ ℝ) |
| 111 | 110 | recnd 11289 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}) →
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) ∈ ℂ) |
| 112 | 90, 12, 108, 109, 111 | fsumf1o 15759 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^3)) → Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) = Σ𝑒 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘((𝐹‘𝑒)‘0)) · ((Λ‘((𝐹‘𝑒)‘1)) · (Λ‘((𝐹‘𝑒)‘2))))) |
| 113 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑒 = 𝑛 → (𝐹‘𝑒) = (𝐹‘𝑛)) |
| 114 | 113 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝑒 = 𝑛 → ((𝐹‘𝑒)‘0) = ((𝐹‘𝑛)‘0)) |
| 115 | 114 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝑒 = 𝑛 → (Λ‘((𝐹‘𝑒)‘0)) = (Λ‘((𝐹‘𝑛)‘0))) |
| 116 | 113 | fveq1d 6908 |
. . . . . . . . . 10
⊢ (𝑒 = 𝑛 → ((𝐹‘𝑒)‘1) = ((𝐹‘𝑛)‘1)) |
| 117 | 116 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑒 = 𝑛 → (Λ‘((𝐹‘𝑒)‘1)) = (Λ‘((𝐹‘𝑛)‘1))) |
| 118 | 113 | fveq1d 6908 |
. . . . . . . . . 10
⊢ (𝑒 = 𝑛 → ((𝐹‘𝑒)‘2) = ((𝐹‘𝑛)‘2)) |
| 119 | 118 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑒 = 𝑛 → (Λ‘((𝐹‘𝑒)‘2)) = (Λ‘((𝐹‘𝑛)‘2))) |
| 120 | 117, 119 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑒 = 𝑛 → ((Λ‘((𝐹‘𝑒)‘1)) · (Λ‘((𝐹‘𝑒)‘2))) = ((Λ‘((𝐹‘𝑛)‘1)) · (Λ‘((𝐹‘𝑛)‘2)))) |
| 121 | 115, 120 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑒 = 𝑛 → ((Λ‘((𝐹‘𝑒)‘0)) · ((Λ‘((𝐹‘𝑒)‘1)) · (Λ‘((𝐹‘𝑒)‘2)))) = ((Λ‘((𝐹‘𝑛)‘0)) · ((Λ‘((𝐹‘𝑛)‘1)) · (Λ‘((𝐹‘𝑛)‘2))))) |
| 122 | 121 | cbvsumv 15732 |
. . . . . 6
⊢
Σ𝑒 ∈
{𝑐 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘((𝐹‘𝑒)‘0)) · ((Λ‘((𝐹‘𝑒)‘1)) · (Λ‘((𝐹‘𝑒)‘2)))) = Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘((𝐹‘𝑛)‘0)) · ((Λ‘((𝐹‘𝑛)‘1)) · (Λ‘((𝐹‘𝑛)‘2)))) |
| 123 | 122 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^3)) → Σ𝑒 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘((𝐹‘𝑒)‘0)) · ((Λ‘((𝐹‘𝑒)‘1)) · (Λ‘((𝐹‘𝑒)‘2)))) = Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘((𝐹‘𝑛)‘0)) · ((Λ‘((𝐹‘𝑛)‘1)) · (Λ‘((𝐹‘𝑛)‘2))))) |
| 124 | | ovexd 7466 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → (0..^3) ∈
V) |
| 125 | 97 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → 𝑎 ∈ (0..^3)) |
| 126 | 124, 125,
26, 106 | pmtridf1o 33114 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) → if(𝑎 = 0, ( I ↾ (0..^3)),
((pmTrsp‘(0..^3))‘{𝑎, 0})):(0..^3)–1-1-onto→(0..^3)) |
| 127 | 107, 126,
21, 14, 19 | hgt750lemg 34669 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^3)) ∧ 𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)}) →
((Λ‘((𝐹‘𝑛)‘0)) · ((Λ‘((𝐹‘𝑛)‘1)) · (Λ‘((𝐹‘𝑛)‘2)))) = ((Λ‘(𝑛‘0)) ·
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) |
| 128 | 127 | sumeq2dv 15738 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^3)) → Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘((𝐹‘𝑛)‘0)) · ((Λ‘((𝐹‘𝑛)‘1)) · (Λ‘((𝐹‘𝑛)‘2)))) = Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) ·
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) |
| 129 | 112, 123,
128 | 3eqtrrd 2782 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^3)) → Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) ·
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) = Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))))) |
| 130 | 129 | sumeq2dv 15738 |
. . 3
⊢ (𝜑 → Σ𝑎 ∈ (0..^3)Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) ·
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) = Σ𝑎 ∈ (0..^3)Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))))) |
| 131 | | hashfzo0 14469 |
. . . . . . 7
⊢ (3 ∈
ℕ0 → (♯‘(0..^3)) = 3) |
| 132 | 5, 131 | ax-mp 5 |
. . . . . 6
⊢
(♯‘(0..^3)) = 3 |
| 133 | 132 | a1i 11 |
. . . . 5
⊢ (𝜑 → (♯‘(0..^3)) =
3) |
| 134 | 133 | eqcomd 2743 |
. . . 4
⊢ (𝜑 → 3 =
(♯‘(0..^3))) |
| 135 | | hgt750lemb.a |
. . . . . 6
⊢ 𝐴 = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩
ℙ)} |
| 136 | 135 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐴 = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩
ℙ)}) |
| 137 | 136 | sumeq1d 15736 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) = Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))))) |
| 138 | 134, 137 | oveq12d 7449 |
. . 3
⊢ (𝜑 → (3 · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))))) = ((♯‘(0..^3))
· Σ𝑛 ∈
{𝑐 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑐‘0)
∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))))) |
| 139 | 82, 130, 138 | 3eqtr4rd 2788 |
. 2
⊢ (𝜑 → (3 · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))))) = Σ𝑎 ∈ (0..^3)Σ𝑛 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) ·
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) |
| 140 | 51, 58, 139 | 3brtr4d 5175 |
1
⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) ·
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ (3 ·
Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) ·
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) |