Step |
Hyp |
Ref |
Expression |
1 |
|
hgt750leme.o |
⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 } |
2 |
|
hgt750leme.n |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
3 |
|
hgt750lemb.2 |
⊢ ( 𝜑 → 2 ≤ 𝑁 ) |
4 |
|
hgt750lemb.a |
⊢ 𝐴 = { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } |
5 |
|
hgt750lema.f |
⊢ 𝐹 = ( 𝑑 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ↦ ( 𝑑 ∘ if ( 𝑎 = 0 , ( I ↾ ( 0 ..^ 3 ) ) , ( ( pmTrsp ‘ ( 0 ..^ 3 ) ) ‘ { 𝑎 , 0 } ) ) ) ) |
6 |
|
fzofi |
⊢ ( 0 ..^ 3 ) ∈ Fin |
7 |
6
|
a1i |
⊢ ( 𝜑 → ( 0 ..^ 3 ) ∈ Fin ) |
8 |
2
|
nnnn0d |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
9 |
|
3nn0 |
⊢ 3 ∈ ℕ0 |
10 |
9
|
a1i |
⊢ ( 𝜑 → 3 ∈ ℕ0 ) |
11 |
|
ssidd |
⊢ ( 𝜑 → ℕ ⊆ ℕ ) |
12 |
8 10 11
|
reprfi2 |
⊢ ( 𝜑 → ( ℕ ( repr ‘ 3 ) 𝑁 ) ∈ Fin ) |
13 |
|
ssrab2 |
⊢ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ⊆ ( ℕ ( repr ‘ 3 ) 𝑁 ) |
14 |
13
|
a1i |
⊢ ( 𝜑 → { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ⊆ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) |
15 |
12 14
|
ssfid |
⊢ ( 𝜑 → { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ∈ Fin ) |
16 |
15
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ∈ Fin ) |
17 |
|
vmaf |
⊢ Λ : ℕ ⟶ ℝ |
18 |
17
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → Λ : ℕ ⟶ ℝ ) |
19 |
|
ssidd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ℕ ⊆ ℕ ) |
20 |
8
|
nn0zd |
⊢ ( 𝜑 → 𝑁 ∈ ℤ ) |
21 |
20
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 𝑁 ∈ ℤ ) |
22 |
9
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 3 ∈ ℕ0 ) |
23 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) |
24 |
13 23
|
sselid |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) |
25 |
19 21 22 24
|
reprf |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 𝑛 : ( 0 ..^ 3 ) ⟶ ℕ ) |
26 |
|
c0ex |
⊢ 0 ∈ V |
27 |
26
|
tpid1 |
⊢ 0 ∈ { 0 , 1 , 2 } |
28 |
|
fzo0to3tp |
⊢ ( 0 ..^ 3 ) = { 0 , 1 , 2 } |
29 |
27 28
|
eleqtrri |
⊢ 0 ∈ ( 0 ..^ 3 ) |
30 |
29
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 0 ∈ ( 0 ..^ 3 ) ) |
31 |
25 30
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( 𝑛 ‘ 0 ) ∈ ℕ ) |
32 |
18 31
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( Λ ‘ ( 𝑛 ‘ 0 ) ) ∈ ℝ ) |
33 |
|
1ex |
⊢ 1 ∈ V |
34 |
33
|
tpid2 |
⊢ 1 ∈ { 0 , 1 , 2 } |
35 |
34 28
|
eleqtrri |
⊢ 1 ∈ ( 0 ..^ 3 ) |
36 |
35
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 1 ∈ ( 0 ..^ 3 ) ) |
37 |
25 36
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( 𝑛 ‘ 1 ) ∈ ℕ ) |
38 |
18 37
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( Λ ‘ ( 𝑛 ‘ 1 ) ) ∈ ℝ ) |
39 |
|
2ex |
⊢ 2 ∈ V |
40 |
39
|
tpid3 |
⊢ 2 ∈ { 0 , 1 , 2 } |
41 |
40 28
|
eleqtrri |
⊢ 2 ∈ ( 0 ..^ 3 ) |
42 |
41
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 2 ∈ ( 0 ..^ 3 ) ) |
43 |
25 42
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( 𝑛 ‘ 2 ) ∈ ℕ ) |
44 |
18 43
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( Λ ‘ ( 𝑛 ‘ 2 ) ) ∈ ℝ ) |
45 |
38 44
|
remulcld |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ∈ ℝ ) |
46 |
32 45
|
remulcld |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ∈ ℝ ) |
47 |
|
vmage0 |
⊢ ( ( 𝑛 ‘ 0 ) ∈ ℕ → 0 ≤ ( Λ ‘ ( 𝑛 ‘ 0 ) ) ) |
48 |
31 47
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 0 ≤ ( Λ ‘ ( 𝑛 ‘ 0 ) ) ) |
49 |
|
vmage0 |
⊢ ( ( 𝑛 ‘ 1 ) ∈ ℕ → 0 ≤ ( Λ ‘ ( 𝑛 ‘ 1 ) ) ) |
50 |
37 49
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 0 ≤ ( Λ ‘ ( 𝑛 ‘ 1 ) ) ) |
51 |
|
vmage0 |
⊢ ( ( 𝑛 ‘ 2 ) ∈ ℕ → 0 ≤ ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) |
52 |
43 51
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 0 ≤ ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) |
53 |
38 44 50 52
|
mulge0d |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 0 ≤ ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) |
54 |
32 45 48 53
|
mulge0d |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 0 ≤ ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) |
55 |
7 16 46 54
|
fsumiunle |
⊢ ( 𝜑 → Σ 𝑛 ∈ ∪ 𝑎 ∈ ( 0 ..^ 3 ) { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ≤ Σ 𝑎 ∈ ( 0 ..^ 3 ) Σ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) |
56 |
|
eqid |
⊢ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } = { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } |
57 |
|
inss2 |
⊢ ( 𝑂 ∩ ℙ ) ⊆ ℙ |
58 |
|
prmssnn |
⊢ ℙ ⊆ ℕ |
59 |
57 58
|
sstri |
⊢ ( 𝑂 ∩ ℙ ) ⊆ ℕ |
60 |
59
|
a1i |
⊢ ( 𝜑 → ( 𝑂 ∩ ℙ ) ⊆ ℕ ) |
61 |
56 11 60 8 10
|
reprdifc |
⊢ ( 𝜑 → ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) = ∪ 𝑎 ∈ ( 0 ..^ 3 ) { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) |
62 |
61
|
sumeq1d |
⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) = Σ 𝑛 ∈ ∪ 𝑎 ∈ ( 0 ..^ 3 ) { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) |
63 |
|
ssrab2 |
⊢ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ⊆ ( ℕ ( repr ‘ 3 ) 𝑁 ) |
64 |
63
|
a1i |
⊢ ( 𝜑 → { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ⊆ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) |
65 |
12 64
|
ssfid |
⊢ ( 𝜑 → { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ∈ Fin ) |
66 |
17
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → Λ : ℕ ⟶ ℝ ) |
67 |
|
ssidd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ℕ ⊆ ℕ ) |
68 |
20
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 𝑁 ∈ ℤ ) |
69 |
9
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 3 ∈ ℕ0 ) |
70 |
64
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) |
71 |
67 68 69 70
|
reprf |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 𝑛 : ( 0 ..^ 3 ) ⟶ ℕ ) |
72 |
29
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 0 ∈ ( 0 ..^ 3 ) ) |
73 |
71 72
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( 𝑛 ‘ 0 ) ∈ ℕ ) |
74 |
66 73
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( Λ ‘ ( 𝑛 ‘ 0 ) ) ∈ ℝ ) |
75 |
35
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 1 ∈ ( 0 ..^ 3 ) ) |
76 |
71 75
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( 𝑛 ‘ 1 ) ∈ ℕ ) |
77 |
66 76
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( Λ ‘ ( 𝑛 ‘ 1 ) ) ∈ ℝ ) |
78 |
41
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 2 ∈ ( 0 ..^ 3 ) ) |
79 |
71 78
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( 𝑛 ‘ 2 ) ∈ ℕ ) |
80 |
66 79
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( Λ ‘ ( 𝑛 ‘ 2 ) ) ∈ ℝ ) |
81 |
77 80
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ∈ ℝ ) |
82 |
74 81
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ∈ ℝ ) |
83 |
65 82
|
fsumrecl |
⊢ ( 𝜑 → Σ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ∈ ℝ ) |
84 |
83
|
recnd |
⊢ ( 𝜑 → Σ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ∈ ℂ ) |
85 |
|
fsumconst |
⊢ ( ( ( 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 ) ) ) ) ) ) |
86 |
7 84 85
|
syl2anc |
⊢ ( 𝜑 → Σ 𝑎 ∈ ( 0 ..^ 3 ) Σ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) = ( ( ♯ ‘ ( 0 ..^ 3 ) ) · Σ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ) |
87 |
|
fveq1 |
⊢ ( 𝑛 = ( 𝐹 ‘ 𝑒 ) → ( 𝑛 ‘ 0 ) = ( ( 𝐹 ‘ 𝑒 ) ‘ 0 ) ) |
88 |
87
|
fveq2d |
⊢ ( 𝑛 = ( 𝐹 ‘ 𝑒 ) → ( Λ ‘ ( 𝑛 ‘ 0 ) ) = ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 0 ) ) ) |
89 |
|
fveq1 |
⊢ ( 𝑛 = ( 𝐹 ‘ 𝑒 ) → ( 𝑛 ‘ 1 ) = ( ( 𝐹 ‘ 𝑒 ) ‘ 1 ) ) |
90 |
89
|
fveq2d |
⊢ ( 𝑛 = ( 𝐹 ‘ 𝑒 ) → ( Λ ‘ ( 𝑛 ‘ 1 ) ) = ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 1 ) ) ) |
91 |
|
fveq1 |
⊢ ( 𝑛 = ( 𝐹 ‘ 𝑒 ) → ( 𝑛 ‘ 2 ) = ( ( 𝐹 ‘ 𝑒 ) ‘ 2 ) ) |
92 |
91
|
fveq2d |
⊢ ( 𝑛 = ( 𝐹 ‘ 𝑒 ) → ( Λ ‘ ( 𝑛 ‘ 2 ) ) = ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 2 ) ) ) |
93 |
90 92
|
oveq12d |
⊢ ( 𝑛 = ( 𝐹 ‘ 𝑒 ) → ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) = ( ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 1 ) ) · ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 2 ) ) ) ) |
94 |
88 93
|
oveq12d |
⊢ ( 𝑛 = ( 𝐹 ‘ 𝑒 ) → ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) = ( ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 0 ) ) · ( ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 1 ) ) · ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 2 ) ) ) ) ) |
95 |
|
3nn |
⊢ 3 ∈ ℕ |
96 |
95
|
a1i |
⊢ ( 𝜑 → 3 ∈ ℕ ) |
97 |
96
|
ralrimivw |
⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 0 ..^ 3 ) 3 ∈ ℕ ) |
98 |
97
|
r19.21bi |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → 3 ∈ ℕ ) |
99 |
20
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → 𝑁 ∈ ℤ ) |
100 |
|
ssidd |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → ℕ ⊆ ℕ ) |
101 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → 𝑎 ∈ ( 0 ..^ 3 ) ) |
102 |
|
fveq1 |
⊢ ( 𝑐 = 𝑑 → ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) |
103 |
102
|
eleq1d |
⊢ ( 𝑐 = 𝑑 → ( ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) ↔ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) ) ) |
104 |
103
|
notbid |
⊢ ( 𝑐 = 𝑑 → ( ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) ↔ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) ) ) |
105 |
104
|
cbvrabv |
⊢ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } = { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } |
106 |
|
fveq1 |
⊢ ( 𝑐 = 𝑑 → ( 𝑐 ‘ 𝑎 ) = ( 𝑑 ‘ 𝑎 ) ) |
107 |
106
|
eleq1d |
⊢ ( 𝑐 = 𝑑 → ( ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) ↔ ( 𝑑 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) ) ) |
108 |
107
|
notbid |
⊢ ( 𝑐 = 𝑑 → ( ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) ↔ ¬ ( 𝑑 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) ) ) |
109 |
108
|
cbvrabv |
⊢ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } = { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } |
110 |
|
eqid |
⊢ if ( 𝑎 = 0 , ( I ↾ ( 0 ..^ 3 ) ) , ( ( pmTrsp ‘ ( 0 ..^ 3 ) ) ‘ { 𝑎 , 0 } ) ) = if ( 𝑎 = 0 , ( I ↾ ( 0 ..^ 3 ) ) , ( ( pmTrsp ‘ ( 0 ..^ 3 ) ) ‘ { 𝑎 , 0 } ) ) |
111 |
98 99 100 101 105 109 110 5
|
reprpmtf1o |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → 𝐹 : { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } –1-1-onto→ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) |
112 |
|
eqidd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑒 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( 𝐹 ‘ 𝑒 ) = ( 𝐹 ‘ 𝑒 ) ) |
113 |
82
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ∈ ℝ ) |
114 |
113
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ∈ ℂ ) |
115 |
94 16 111 112 114
|
fsumf1o |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → Σ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) = Σ 𝑒 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 0 ) ) · ( ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 1 ) ) · ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 2 ) ) ) ) ) |
116 |
|
fveq2 |
⊢ ( 𝑒 = 𝑛 → ( 𝐹 ‘ 𝑒 ) = ( 𝐹 ‘ 𝑛 ) ) |
117 |
116
|
fveq1d |
⊢ ( 𝑒 = 𝑛 → ( ( 𝐹 ‘ 𝑒 ) ‘ 0 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 0 ) ) |
118 |
117
|
fveq2d |
⊢ ( 𝑒 = 𝑛 → ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 0 ) ) = ( Λ ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 0 ) ) ) |
119 |
116
|
fveq1d |
⊢ ( 𝑒 = 𝑛 → ( ( 𝐹 ‘ 𝑒 ) ‘ 1 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 1 ) ) |
120 |
119
|
fveq2d |
⊢ ( 𝑒 = 𝑛 → ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 1 ) ) = ( Λ ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 1 ) ) ) |
121 |
116
|
fveq1d |
⊢ ( 𝑒 = 𝑛 → ( ( 𝐹 ‘ 𝑒 ) ‘ 2 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 2 ) ) |
122 |
121
|
fveq2d |
⊢ ( 𝑒 = 𝑛 → ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 2 ) ) = ( Λ ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 2 ) ) ) |
123 |
120 122
|
oveq12d |
⊢ ( 𝑒 = 𝑛 → ( ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 1 ) ) · ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 2 ) ) ) = ( ( Λ ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 1 ) ) · ( Λ ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 2 ) ) ) ) |
124 |
118 123
|
oveq12d |
⊢ ( 𝑒 = 𝑛 → ( ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 0 ) ) · ( ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 1 ) ) · ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 2 ) ) ) ) = ( ( Λ ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 0 ) ) · ( ( Λ ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 1 ) ) · ( Λ ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 2 ) ) ) ) ) |
125 |
124
|
cbvsumv |
⊢ Σ 𝑒 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 0 ) ) · ( ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 1 ) ) · ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 2 ) ) ) ) = Σ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 0 ) ) · ( ( Λ ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 1 ) ) · ( Λ ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 2 ) ) ) ) |
126 |
125
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → Σ 𝑒 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 0 ) ) · ( ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 1 ) ) · ( Λ ‘ ( ( 𝐹 ‘ 𝑒 ) ‘ 2 ) ) ) ) = Σ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 0 ) ) · ( ( Λ ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 1 ) ) · ( Λ ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 2 ) ) ) ) ) |
127 |
|
ovexd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( 0 ..^ 3 ) ∈ V ) |
128 |
101
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 𝑎 ∈ ( 0 ..^ 3 ) ) |
129 |
127 128 30 110
|
pmtridf1o |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → if ( 𝑎 = 0 , ( I ↾ ( 0 ..^ 3 ) ) , ( ( pmTrsp ‘ ( 0 ..^ 3 ) ) ‘ { 𝑎 , 0 } ) ) : ( 0 ..^ 3 ) –1-1-onto→ ( 0 ..^ 3 ) ) |
130 |
5 129 25 18 23
|
hgt750lemg |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) ∧ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( ( Λ ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 0 ) ) · ( ( Λ ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 1 ) ) · ( Λ ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 2 ) ) ) ) = ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) |
131 |
130
|
sumeq2dv |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → Σ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 0 ) ) · ( ( Λ ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 1 ) ) · ( Λ ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 2 ) ) ) ) = Σ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) |
132 |
115 126 131
|
3eqtrrd |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 3 ) ) → Σ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) = Σ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) |
133 |
132
|
sumeq2dv |
⊢ ( 𝜑 → Σ 𝑎 ∈ ( 0 ..^ 3 ) Σ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) = Σ 𝑎 ∈ ( 0 ..^ 3 ) Σ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) |
134 |
|
hashfzo0 |
⊢ ( 3 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 3 ) ) = 3 ) |
135 |
9 134
|
ax-mp |
⊢ ( ♯ ‘ ( 0 ..^ 3 ) ) = 3 |
136 |
135
|
a1i |
⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ 3 ) ) = 3 ) |
137 |
136
|
eqcomd |
⊢ ( 𝜑 → 3 = ( ♯ ‘ ( 0 ..^ 3 ) ) ) |
138 |
4
|
a1i |
⊢ ( 𝜑 → 𝐴 = { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) |
139 |
138
|
sumeq1d |
⊢ ( 𝜑 → Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) = Σ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) |
140 |
137 139
|
oveq12d |
⊢ ( 𝜑 → ( 3 · Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) = ( ( ♯ ‘ ( 0 ..^ 3 ) ) · Σ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ) |
141 |
86 133 140
|
3eqtr4rd |
⊢ ( 𝜑 → ( 3 · Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) = Σ 𝑎 ∈ ( 0 ..^ 3 ) Σ 𝑛 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) |
142 |
55 62 141
|
3brtr4d |
⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ≤ ( 3 · Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ) |