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 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 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 ) ) ) ) ) )