Metamath Proof Explorer


Theorem hgt750lema

Description: An upper bound on the contribution of the non-prime terms in the Statement 7.50 of Helfgott p. 69. (Contributed by Thierry Arnoux, 1-Jan-2022)

Ref Expression
Hypotheses hgt750leme.o 𝑂 = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
hgt750leme.n ( 𝜑𝑁 ∈ ℕ )
hgt750lemb.2 ( 𝜑 → 2 ≤ 𝑁 )
hgt750lemb.a 𝐴 = { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) }
hgt750lema.f 𝐹 = ( 𝑑 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ↦ ( 𝑑 ∘ if ( 𝑎 = 0 , ( I ↾ ( 0 ..^ 3 ) ) , ( ( pmTrsp ‘ ( 0 ..^ 3 ) ) ‘ { 𝑎 , 0 } ) ) ) )
Assertion hgt750lema ( 𝜑 → Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ≤ ( 3 · Σ 𝑛𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )

Proof

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 ) ) ) ) ) )