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