Metamath Proof Explorer

Theorem hgt750lemb

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, 28-Dec-2021)

Ref Expression
Hypotheses hgt750leme.o ⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
hgt750leme.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
hgt750lemb.2 ⊢ ( 𝜑 → 2 ≤ 𝑁 )
hgt750lemb.a ⊢ 𝐴 = { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) }
Assertion hgt750lemb ( 𝜑 → Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ≤ ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) )

Proof

Step Hyp Ref Expression
1 hgt750leme.o ⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
2 hgt750leme.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 hgt750lemb.2 ⊢ ( 𝜑 → 2 ≤ 𝑁 )
4 hgt750lemb.a ⊢ 𝐴 = { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) }
5 2 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6 3nn0 ⊢ 3 ∈ ℕ0
7 6 a1i ⊢ ( 𝜑 → 3 ∈ ℕ0 )
8 ssidd ⊢ ( 𝜑 → ℕ ⊆ ℕ )
9 5 7 8 reprfi2 ⊢ ( 𝜑 → ( ℕ ( repr ‘ 3 ) 𝑁 ) ∈ Fin )
10 4 ssrab3 ⊢ 𝐴 ⊆ ( ℕ ( repr ‘ 3 ) 𝑁 )
11 ssfi ⊢ ( ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∈ Fin ∧ 𝐴 ⊆ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → 𝐴 ∈ Fin )
12 9 10 11 sylancl ⊢ ( 𝜑 → 𝐴 ∈ Fin )
13 vmaf ⊢ Λ : ℕ ⟶ ℝ
14 13 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → Λ : ℕ ⟶ ℝ )
15 ssidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ℕ ⊆ ℕ )
16 2 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 𝑁 ∈ ℤ )
18 6 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 3 ∈ ℕ0 )
19 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 𝑛 ∈ 𝐴 )
20 10 19 sselid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) )
21 15 17 18 20 reprf ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 𝑛 : ( 0 ..^ 3 ) ⟶ ℕ )
22 c0ex ⊢ 0 ∈ V
23 22 tpid1 ⊢ 0 ∈ { 0 , 1 , 2 }
24 fzo0to3tp ⊢ ( 0 ..^ 3 ) = { 0 , 1 , 2 }
25 23 24 eleqtrri ⊢ 0 ∈ ( 0 ..^ 3 )
26 25 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 0 ∈ ( 0 ..^ 3 ) )
27 21 26 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝑛 ‘ 0 ) ∈ ℕ )
28 14 27 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( Λ ‘ ( 𝑛 ‘ 0 ) ) ∈ ℝ )
29 1eltp012 ⊢ 1 ∈ { 0 , 1 , 2 }
30 29 24 eleqtrri ⊢ 1 ∈ ( 0 ..^ 3 )
31 30 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 1 ∈ ( 0 ..^ 3 ) )
32 21 31 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝑛 ‘ 1 ) ∈ ℕ )
33 14 32 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( Λ ‘ ( 𝑛 ‘ 1 ) ) ∈ ℝ )
34 2ex ⊢ 2 ∈ V
35 34 tpid3 ⊢ 2 ∈ { 0 , 1 , 2 }
36 35 24 eleqtrri ⊢ 2 ∈ ( 0 ..^ 3 )
37 36 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 2 ∈ ( 0 ..^ 3 ) )
38 21 37 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝑛 ‘ 2 ) ∈ ℕ )
39 14 38 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( Λ ‘ ( 𝑛 ‘ 2 ) ) ∈ ℝ )
40 33 39 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ∈ ℝ )
41 28 40 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ∈ ℝ )
42 12 41 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ∈ ℝ )
43 2 nnrpd ⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
44 43 relogcld ⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℝ )
45 28 33 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( Λ ‘ ( 𝑛 ‘ 1 ) ) ) ∈ ℝ )
46 12 45 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( Λ ‘ ( 𝑛 ‘ 1 ) ) ) ∈ ℝ )
47 44 46 remulcld ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) · Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( Λ ‘ ( 𝑛 ‘ 1 ) ) ) ) ∈ ℝ )
48 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
49 diffi ⊢ ( ( 1 ... 𝑁 ) ∈ Fin → ( ( 1 ... 𝑁 ) ∖ ℙ ) ∈ Fin )
50 48 49 ax-mp ⊢ ( ( 1 ... 𝑁 ) ∖ ℙ ) ∈ Fin
51 snfi ⊢ { 2 } ∈ Fin
52 unfi ⊢ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∈ Fin ∧ { 2 } ∈ Fin ) → ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ∈ Fin )
53 50 51 52 mp2an ⊢ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ∈ Fin
54 53 a1i ⊢ ( 𝜑 → ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ∈ Fin )
55 13 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ) → Λ : ℕ ⟶ ℝ )
56 difss ⊢ ( ( 1 ... 𝑁 ) ∖ ℙ ) ⊆ ( 1 ... 𝑁 )
57 56 a1i ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ ℙ ) ⊆ ( 1 ... 𝑁 ) )
58 2nn ⊢ 2 ∈ ℕ
59 58 a1i ⊢ ( 𝜑 → 2 ∈ ℕ )
60 elfz1b ⊢ ( 2 ∈ ( 1 ... 𝑁 ) ↔ ( 2 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 2 ≤ 𝑁 ) )
61 60 biimpri ⊢ ( ( 2 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 2 ≤ 𝑁 ) → 2 ∈ ( 1 ... 𝑁 ) )
62 59 2 3 61 syl3anc ⊢ ( 𝜑 → 2 ∈ ( 1 ... 𝑁 ) )
63 62 snssd ⊢ ( 𝜑 → { 2 } ⊆ ( 1 ... 𝑁 ) )
64 57 63 unssd ⊢ ( 𝜑 → ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ⊆ ( 1 ... 𝑁 ) )
65 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
66 65 a1i ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ⊆ ℕ )
67 64 66 sstrd ⊢ ( 𝜑 → ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ⊆ ℕ )
68 67 sselda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ) → 𝑖 ∈ ℕ )
69 55 68 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ) → ( Λ ‘ 𝑖 ) ∈ ℝ )
70 54 69 fsumrecl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) ∈ ℝ )
71 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
72 13 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → Λ : ℕ ⟶ ℝ )
73 66 sselda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑗 ∈ ℕ )
74 72 73 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( Λ ‘ 𝑗 ) ∈ ℝ )
75 71 74 fsumrecl ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ∈ ℝ )
76 70 75 remulcld ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ∈ ℝ )
77 44 76 remulcld ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) ∈ ℝ )
78 2 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 𝑁 ∈ ℕ )
79 78 nnrpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 𝑁 ∈ ℝ+ )
80 relogcl ⊢ ( 𝑁 ∈ ℝ+ → ( log ‘ 𝑁 ) ∈ ℝ )
81 79 80 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( log ‘ 𝑁 ) ∈ ℝ )
82 33 81 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( log ‘ 𝑁 ) ) ∈ ℝ )
83 28 82 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( log ‘ 𝑁 ) ) ) ∈ ℝ )
84 vmage0 ⊢ ( ( 𝑛 ‘ 0 ) ∈ ℕ → 0 ≤ ( Λ ‘ ( 𝑛 ‘ 0 ) ) )
85 27 84 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 0 ≤ ( Λ ‘ ( 𝑛 ‘ 0 ) ) )
86 vmage0 ⊢ ( ( 𝑛 ‘ 1 ) ∈ ℕ → 0 ≤ ( Λ ‘ ( 𝑛 ‘ 1 ) ) )
87 32 86 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 0 ≤ ( Λ ‘ ( 𝑛 ‘ 1 ) ) )
88 38 nnrpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝑛 ‘ 2 ) ∈ ℝ+ )
89 88 relogcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( log ‘ ( 𝑛 ‘ 2 ) ) ∈ ℝ )
90 vmalelog ⊢ ( ( 𝑛 ‘ 2 ) ∈ ℕ → ( Λ ‘ ( 𝑛 ‘ 2 ) ) ≤ ( log ‘ ( 𝑛 ‘ 2 ) ) )
91 38 90 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( Λ ‘ ( 𝑛 ‘ 2 ) ) ≤ ( log ‘ ( 𝑛 ‘ 2 ) ) )
92 15 17 18 20 37 reprle ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝑛 ‘ 2 ) ≤ 𝑁 )
93 logleb ⊢ ( ( ( 𝑛 ‘ 2 ) ∈ ℝ+ ∧ 𝑁 ∈ ℝ+ ) → ( ( 𝑛 ‘ 2 ) ≤ 𝑁 ↔ ( log ‘ ( 𝑛 ‘ 2 ) ) ≤ ( log ‘ 𝑁 ) ) )
94 93 biimpa ⊢ ( ( ( ( 𝑛 ‘ 2 ) ∈ ℝ+ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 𝑛 ‘ 2 ) ≤ 𝑁 ) → ( log ‘ ( 𝑛 ‘ 2 ) ) ≤ ( log ‘ 𝑁 ) )
95 88 79 92 94 syl21anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( log ‘ ( 𝑛 ‘ 2 ) ) ≤ ( log ‘ 𝑁 ) )
96 39 89 81 91 95 letrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( Λ ‘ ( 𝑛 ‘ 2 ) ) ≤ ( log ‘ 𝑁 ) )
97 39 81 33 87 96 lemul2ad ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ≤ ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( log ‘ 𝑁 ) ) )
98 40 82 28 85 97 lemul2ad ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ≤ ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( log ‘ 𝑁 ) ) ) )
99 12 41 83 98 fsumle ⊢ ( 𝜑 → Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ≤ Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( log ‘ 𝑁 ) ) ) )
100 2 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
101 2 nnne0d ⊢ ( 𝜑 → 𝑁 ≠ 0 )
102 100 101 logcld ⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℂ )
103 45 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( Λ ‘ ( 𝑛 ‘ 1 ) ) ) ∈ ℂ )
104 12 102 103 fsummulc2 ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) · Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( Λ ‘ ( 𝑛 ‘ 1 ) ) ) ) = Σ 𝑛 ∈ 𝐴 ( ( log ‘ 𝑁 ) · ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( Λ ‘ ( 𝑛 ‘ 1 ) ) ) ) )
105 102 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( log ‘ 𝑁 ) ∈ ℂ )
106 105 103 mulcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( log ‘ 𝑁 ) · ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( Λ ‘ ( 𝑛 ‘ 1 ) ) ) ) = ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( Λ ‘ ( 𝑛 ‘ 1 ) ) ) · ( log ‘ 𝑁 ) ) )
107 28 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( Λ ‘ ( 𝑛 ‘ 0 ) ) ∈ ℂ )
108 33 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( Λ ‘ ( 𝑛 ‘ 1 ) ) ∈ ℂ )
109 107 108 105 mulassd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( Λ ‘ ( 𝑛 ‘ 1 ) ) ) · ( log ‘ 𝑁 ) ) = ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( log ‘ 𝑁 ) ) ) )
110 106 109 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( log ‘ 𝑁 ) · ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( Λ ‘ ( 𝑛 ‘ 1 ) ) ) ) = ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( log ‘ 𝑁 ) ) ) )
111 110 sumeq2dv ⊢ ( 𝜑 → Σ 𝑛 ∈ 𝐴 ( ( log ‘ 𝑁 ) · ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( Λ ‘ ( 𝑛 ‘ 1 ) ) ) ) = Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( log ‘ 𝑁 ) ) ) )
112 104 111 eqtr2d ⊢ ( 𝜑 → Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( log ‘ 𝑁 ) ) ) = ( ( log ‘ 𝑁 ) · Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( Λ ‘ ( 𝑛 ‘ 1 ) ) ) ) )
113 99 112 breqtrd ⊢ ( 𝜑 → Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ≤ ( ( log ‘ 𝑁 ) · Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( Λ ‘ ( 𝑛 ‘ 1 ) ) ) ) )
114 2 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
115 2 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝑁 )
116 114 115 logge0d ⊢ ( 𝜑 → 0 ≤ ( log ‘ 𝑁 ) )
117 xpfi ⊢ ( ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ∈ Fin ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) ∈ Fin )
118 54 71 117 syl2anc ⊢ ( 𝜑 → ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) ∈ Fin )
119 13 a1i ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) ) → Λ : ℕ ⟶ ℝ )
120 67 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) ) → ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ⊆ ℕ )
121 xp1st ⊢ ( 𝑢 ∈ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) → ( 1st ‘ 𝑢 ) ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) )
122 121 adantl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) ) → ( 1st ‘ 𝑢 ) ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) )
123 120 122 sseldd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) ) → ( 1st ‘ 𝑢 ) ∈ ℕ )
124 119 123 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) ) → ( Λ ‘ ( 1st ‘ 𝑢 ) ) ∈ ℝ )
125 xp2nd ⊢ ( 𝑢 ∈ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) → ( 2nd ‘ 𝑢 ) ∈ ( 1 ... 𝑁 ) )
126 125 adantl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) ) → ( 2nd ‘ 𝑢 ) ∈ ( 1 ... 𝑁 ) )
127 65 126 sselid ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) ) → ( 2nd ‘ 𝑢 ) ∈ ℕ )
128 119 127 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) ) → ( Λ ‘ ( 2nd ‘ 𝑢 ) ) ∈ ℝ )
129 124 128 remulcld ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) ) → ( ( Λ ‘ ( 1st ‘ 𝑢 ) ) · ( Λ ‘ ( 2nd ‘ 𝑢 ) ) ) ∈ ℝ )
130 vmage0 ⊢ ( ( 1st ‘ 𝑢 ) ∈ ℕ → 0 ≤ ( Λ ‘ ( 1st ‘ 𝑢 ) ) )
131 123 130 syl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) ) → 0 ≤ ( Λ ‘ ( 1st ‘ 𝑢 ) ) )
132 vmage0 ⊢ ( ( 2nd ‘ 𝑢 ) ∈ ℕ → 0 ≤ ( Λ ‘ ( 2nd ‘ 𝑢 ) ) )
133 127 132 syl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) ) → 0 ≤ ( Λ ‘ ( 2nd ‘ 𝑢 ) ) )
134 124 128 131 133 mulge0d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) ) → 0 ≤ ( ( Λ ‘ ( 1st ‘ 𝑢 ) ) · ( Λ ‘ ( 2nd ‘ 𝑢 ) ) ) )
135 ssidd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ℕ ⊆ ℕ )
136 16 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 𝑁 ∈ ℤ )
137 6 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 3 ∈ ℕ0 )
138 simpr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 𝑐 ∈ 𝐴 )
139 10 138 sselid ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) )
140 135 136 137 139 reprf ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 𝑐 : ( 0 ..^ 3 ) ⟶ ℕ )
141 25 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 0 ∈ ( 0 ..^ 3 ) )
142 140 141 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑐 ‘ 0 ) ∈ ℕ )
143 2 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 𝑁 ∈ ℕ )
144 135 136 137 139 141 reprle ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑐 ‘ 0 ) ≤ 𝑁 )
145 elfz1b ⊢ ( ( 𝑐 ‘ 0 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝑐 ‘ 0 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑐 ‘ 0 ) ≤ 𝑁 ) )
146 145 biimpri ⊢ ( ( ( 𝑐 ‘ 0 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑐 ‘ 0 ) ≤ 𝑁 ) → ( 𝑐 ‘ 0 ) ∈ ( 1 ... 𝑁 ) )
147 142 143 144 146 syl3anc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑐 ‘ 0 ) ∈ ( 1 ... 𝑁 ) )
148 4 reqabi ⊢ ( 𝑐 ∈ 𝐴 ↔ ( 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∧ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) ) )
149 148 simprbi ⊢ ( 𝑐 ∈ 𝐴 → ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) )
150 1 oddprm2 ⊢ ( ℙ ∖ { 2 } ) = ( 𝑂 ∩ ℙ )
151 150 eleq2i ⊢ ( ( 𝑐 ‘ 0 ) ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) )
152 149 151 sylnibr ⊢ ( 𝑐 ∈ 𝐴 → ¬ ( 𝑐 ‘ 0 ) ∈ ( ℙ ∖ { 2 } ) )
153 138 152 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ¬ ( 𝑐 ‘ 0 ) ∈ ( ℙ ∖ { 2 } ) )
154 147 153 jca ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( ( 𝑐 ‘ 0 ) ∈ ( 1 ... 𝑁 ) ∧ ¬ ( 𝑐 ‘ 0 ) ∈ ( ℙ ∖ { 2 } ) ) )
155 eldif ⊢ ( ( 𝑐 ‘ 0 ) ∈ ( ( 1 ... 𝑁 ) ∖ ( ℙ ∖ { 2 } ) ) ↔ ( ( 𝑐 ‘ 0 ) ∈ ( 1 ... 𝑁 ) ∧ ¬ ( 𝑐 ‘ 0 ) ∈ ( ℙ ∖ { 2 } ) ) )
156 154 155 sylibr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑐 ‘ 0 ) ∈ ( ( 1 ... 𝑁 ) ∖ ( ℙ ∖ { 2 } ) ) )
157 uncom ⊢ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) = ( { 2 } ∪ ( ( 1 ... 𝑁 ) ∖ ℙ ) )
158 undif3 ⊢ ( { 2 } ∪ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) = ( ( { 2 } ∪ ( 1 ... 𝑁 ) ) ∖ ( ℙ ∖ { 2 } ) )
159 157 158 eqtri ⊢ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) = ( ( { 2 } ∪ ( 1 ... 𝑁 ) ) ∖ ( ℙ ∖ { 2 } ) )
160 ssequn1 ⊢ ( { 2 } ⊆ ( 1 ... 𝑁 ) ↔ ( { 2 } ∪ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
161 63 160 sylib ⊢ ( 𝜑 → ( { 2 } ∪ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
162 161 difeq1d ⊢ ( 𝜑 → ( ( { 2 } ∪ ( 1 ... 𝑁 ) ) ∖ ( ℙ ∖ { 2 } ) ) = ( ( 1 ... 𝑁 ) ∖ ( ℙ ∖ { 2 } ) ) )
163 159 162 eqtrid ⊢ ( 𝜑 → ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) = ( ( 1 ... 𝑁 ) ∖ ( ℙ ∖ { 2 } ) ) )
164 163 eleq2d ⊢ ( 𝜑 → ( ( 𝑐 ‘ 0 ) ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ↔ ( 𝑐 ‘ 0 ) ∈ ( ( 1 ... 𝑁 ) ∖ ( ℙ ∖ { 2 } ) ) ) )
165 164 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( ( 𝑐 ‘ 0 ) ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ↔ ( 𝑐 ‘ 0 ) ∈ ( ( 1 ... 𝑁 ) ∖ ( ℙ ∖ { 2 } ) ) ) )
166 156 165 mpbird ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑐 ‘ 0 ) ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) )
167 30 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 1 ∈ ( 0 ..^ 3 ) )
168 140 167 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑐 ‘ 1 ) ∈ ℕ )
169 135 136 137 139 167 reprle ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑐 ‘ 1 ) ≤ 𝑁 )
170 elfz1b ⊢ ( ( 𝑐 ‘ 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝑐 ‘ 1 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑐 ‘ 1 ) ≤ 𝑁 ) )
171 170 biimpri ⊢ ( ( ( 𝑐 ‘ 1 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑐 ‘ 1 ) ≤ 𝑁 ) → ( 𝑐 ‘ 1 ) ∈ ( 1 ... 𝑁 ) )
172 168 143 169 171 syl3anc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑐 ‘ 1 ) ∈ ( 1 ... 𝑁 ) )
173 166 172 opelxpd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ⟨ ( 𝑐 ‘ 0 ) , ( 𝑐 ‘ 1 ) ⟩ ∈ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) )
174 173 ralrimiva ⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝐴 ⟨ ( 𝑐 ‘ 0 ) , ( 𝑐 ‘ 1 ) ⟩ ∈ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) )
175 fveq1 ⊢ ( 𝑑 = 𝑐 → ( 𝑑 ‘ 0 ) = ( 𝑐 ‘ 0 ) )
176 fveq1 ⊢ ( 𝑑 = 𝑐 → ( 𝑑 ‘ 1 ) = ( 𝑐 ‘ 1 ) )
177 175 176 opeq12d ⊢ ( 𝑑 = 𝑐 → ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ = ⟨ ( 𝑐 ‘ 0 ) , ( 𝑐 ‘ 1 ) ⟩ )
178 177 cbvmptv ⊢ ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) = ( 𝑐 ∈ 𝐴 ↦ ⟨ ( 𝑐 ‘ 0 ) , ( 𝑐 ‘ 1 ) ⟩ )
179 178 rnmptss ⊢ ( ∀ 𝑐 ∈ 𝐴 ⟨ ( 𝑐 ‘ 0 ) , ( 𝑐 ‘ 1 ) ⟩ ∈ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) → ran ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ⊆ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) )
180 174 179 syl ⊢ ( 𝜑 → ran ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ⊆ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) )
181 118 129 134 180 fsumless ⊢ ( 𝜑 → Σ 𝑢 ∈ ran ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ( ( Λ ‘ ( 1st ‘ 𝑢 ) ) · ( Λ ‘ ( 2nd ‘ 𝑢 ) ) ) ≤ Σ 𝑢 ∈ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) ( ( Λ ‘ ( 1st ‘ 𝑢 ) ) · ( Λ ‘ ( 2nd ‘ 𝑢 ) ) ) )
182 fvex ⊢ ( 𝑛 ‘ 0 ) ∈ V
183 fvex ⊢ ( 𝑛 ‘ 1 ) ∈ V
184 182 183 op1std ⊢ ( 𝑢 = ⟨ ( 𝑛 ‘ 0 ) , ( 𝑛 ‘ 1 ) ⟩ → ( 1st ‘ 𝑢 ) = ( 𝑛 ‘ 0 ) )
185 184 fveq2d ⊢ ( 𝑢 = ⟨ ( 𝑛 ‘ 0 ) , ( 𝑛 ‘ 1 ) ⟩ → ( Λ ‘ ( 1st ‘ 𝑢 ) ) = ( Λ ‘ ( 𝑛 ‘ 0 ) ) )
186 182 183 op2ndd ⊢ ( 𝑢 = ⟨ ( 𝑛 ‘ 0 ) , ( 𝑛 ‘ 1 ) ⟩ → ( 2nd ‘ 𝑢 ) = ( 𝑛 ‘ 1 ) )
187 186 fveq2d ⊢ ( 𝑢 = ⟨ ( 𝑛 ‘ 0 ) , ( 𝑛 ‘ 1 ) ⟩ → ( Λ ‘ ( 2nd ‘ 𝑢 ) ) = ( Λ ‘ ( 𝑛 ‘ 1 ) ) )
188 185 187 oveq12d ⊢ ( 𝑢 = ⟨ ( 𝑛 ‘ 0 ) , ( 𝑛 ‘ 1 ) ⟩ → ( ( Λ ‘ ( 1st ‘ 𝑢 ) ) · ( Λ ‘ ( 2nd ‘ 𝑢 ) ) ) = ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( Λ ‘ ( 𝑛 ‘ 1 ) ) ) )
189 opex ⊢ ⟨ ( 𝑐 ‘ 0 ) , ( 𝑐 ‘ 1 ) ⟩ ∈ V
190 189 rgenw ⊢ ∀ 𝑐 ∈ 𝐴 ⟨ ( 𝑐 ‘ 0 ) , ( 𝑐 ‘ 1 ) ⟩ ∈ V
191 178 fnmpt ⊢ ( ∀ 𝑐 ∈ 𝐴 ⟨ ( 𝑐 ‘ 0 ) , ( 𝑐 ‘ 1 ) ⟩ ∈ V → ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) Fn 𝐴 )
192 190 191 mp1i ⊢ ( 𝜑 → ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) Fn 𝐴 )
193 eqidd ⊢ ( 𝜑 → ran ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) = ran ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) )
194 140 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) → 𝑐 : ( 0 ..^ 3 ) ⟶ ℕ )
195 194 ffnd ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) → 𝑐 Fn ( 0 ..^ 3 ) )
196 21 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) → 𝑛 : ( 0 ..^ 3 ) ⟶ ℕ )
197 196 ffnd ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) → 𝑛 Fn ( 0 ..^ 3 ) )
198 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) → ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) )
199 178 a1i ⊢ ( 𝜑 → ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) = ( 𝑐 ∈ 𝐴 ↦ ⟨ ( 𝑐 ‘ 0 ) , ( 𝑐 ‘ 1 ) ⟩ ) )
200 189 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ⟨ ( 𝑐 ‘ 0 ) , ( 𝑐 ‘ 1 ) ⟩ ∈ V )
201 199 200 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ⟨ ( 𝑐 ‘ 0 ) , ( 𝑐 ‘ 1 ) ⟩ )
202 201 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) → ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ⟨ ( 𝑐 ‘ 0 ) , ( 𝑐 ‘ 1 ) ⟩ )
203 202 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) → ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ⟨ ( 𝑐 ‘ 0 ) , ( 𝑐 ‘ 1 ) ⟩ )
204 fveq1 ⊢ ( 𝑐 = 𝑛 → ( 𝑐 ‘ 0 ) = ( 𝑛 ‘ 0 ) )
205 fveq1 ⊢ ( 𝑐 = 𝑛 → ( 𝑐 ‘ 1 ) = ( 𝑛 ‘ 1 ) )
206 204 205 opeq12d ⊢ ( 𝑐 = 𝑛 → ⟨ ( 𝑐 ‘ 0 ) , ( 𝑐 ‘ 1 ) ⟩ = ⟨ ( 𝑛 ‘ 0 ) , ( 𝑛 ‘ 1 ) ⟩ )
207 opex ⊢ ⟨ ( 𝑛 ‘ 0 ) , ( 𝑛 ‘ 1 ) ⟩ ∈ V
208 207 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ⟨ ( 𝑛 ‘ 0 ) , ( 𝑛 ‘ 1 ) ⟩ ∈ V )
209 178 206 19 208 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) = ⟨ ( 𝑛 ‘ 0 ) , ( 𝑛 ‘ 1 ) ⟩ )
210 209 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) → ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) = ⟨ ( 𝑛 ‘ 0 ) , ( 𝑛 ‘ 1 ) ⟩ )
211 210 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) → ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) = ⟨ ( 𝑛 ‘ 0 ) , ( 𝑛 ‘ 1 ) ⟩ )
212 198 203 211 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) → ⟨ ( 𝑐 ‘ 0 ) , ( 𝑐 ‘ 1 ) ⟩ = ⟨ ( 𝑛 ‘ 0 ) , ( 𝑛 ‘ 1 ) ⟩ )
213 182 183 opth2 ⊢ ( ⟨ ( 𝑐 ‘ 0 ) , ( 𝑐 ‘ 1 ) ⟩ = ⟨ ( 𝑛 ‘ 0 ) , ( 𝑛 ‘ 1 ) ⟩ ↔ ( ( 𝑐 ‘ 0 ) = ( 𝑛 ‘ 0 ) ∧ ( 𝑐 ‘ 1 ) = ( 𝑛 ‘ 1 ) ) )
214 212 213 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) → ( ( 𝑐 ‘ 0 ) = ( 𝑛 ‘ 0 ) ∧ ( 𝑐 ‘ 1 ) = ( 𝑛 ‘ 1 ) ) )
215 214 simpld ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) → ( 𝑐 ‘ 0 ) = ( 𝑛 ‘ 0 ) )
216 215 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 0 ) → ( 𝑐 ‘ 0 ) = ( 𝑛 ‘ 0 ) )
217 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 0 ) → 𝑖 = 0 )
218 217 fveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 0 ) → ( 𝑐 ‘ 𝑖 ) = ( 𝑐 ‘ 0 ) )
219 217 fveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 0 ) → ( 𝑛 ‘ 𝑖 ) = ( 𝑛 ‘ 0 ) )
220 216 218 219 3eqtr4d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 0 ) → ( 𝑐 ‘ 𝑖 ) = ( 𝑛 ‘ 𝑖 ) )
221 214 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) → ( 𝑐 ‘ 1 ) = ( 𝑛 ‘ 1 ) )
222 221 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 1 ) → ( 𝑐 ‘ 1 ) = ( 𝑛 ‘ 1 ) )
223 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 1 ) → 𝑖 = 1 )
224 223 fveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 1 ) → ( 𝑐 ‘ 𝑖 ) = ( 𝑐 ‘ 1 ) )
225 223 fveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 1 ) → ( 𝑛 ‘ 𝑖 ) = ( 𝑛 ‘ 1 ) )
226 222 224 225 3eqtr4d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 1 ) → ( 𝑐 ‘ 𝑖 ) = ( 𝑛 ‘ 𝑖 ) )
227 215 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( 𝑐 ‘ 0 ) = ( 𝑛 ‘ 0 ) )
228 221 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( 𝑐 ‘ 1 ) = ( 𝑛 ‘ 1 ) )
229 227 228 oveq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) = ( ( 𝑛 ‘ 0 ) + ( 𝑛 ‘ 1 ) ) )
230 229 oveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( 𝑁 − ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) ) = ( 𝑁 − ( ( 𝑛 ‘ 0 ) + ( 𝑛 ‘ 1 ) ) ) )
231 24 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( 0 ..^ 3 ) = { 0 , 1 , 2 } )
232 231 sumeq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → Σ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑐 ‘ 𝑗 ) = Σ 𝑗 ∈ { 0 , 1 , 2 } ( 𝑐 ‘ 𝑗 ) )
233 ssidd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ℕ ⊆ ℕ )
234 136 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → 𝑁 ∈ ℤ )
235 6 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → 3 ∈ ℕ0 )
236 139 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) )
237 233 234 235 236 reprsum ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → Σ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 )
238 fveq2 ⊢ ( 𝑗 = 0 → ( 𝑐 ‘ 𝑗 ) = ( 𝑐 ‘ 0 ) )
239 fveq2 ⊢ ( 𝑗 = 1 → ( 𝑐 ‘ 𝑗 ) = ( 𝑐 ‘ 1 ) )
240 fveq2 ⊢ ( 𝑗 = 2 → ( 𝑐 ‘ 𝑗 ) = ( 𝑐 ‘ 2 ) )
241 142 nncnd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑐 ‘ 0 ) ∈ ℂ )
242 241 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( 𝑐 ‘ 0 ) ∈ ℂ )
243 168 nncnd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑐 ‘ 1 ) ∈ ℂ )
244 243 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( 𝑐 ‘ 1 ) ∈ ℂ )
245 36 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 2 ∈ ( 0 ..^ 3 ) )
246 140 245 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑐 ‘ 2 ) ∈ ℕ )
247 246 nncnd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑐 ‘ 2 ) ∈ ℂ )
248 247 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( 𝑐 ‘ 2 ) ∈ ℂ )
249 242 244 248 3jca ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( ( 𝑐 ‘ 0 ) ∈ ℂ ∧ ( 𝑐 ‘ 1 ) ∈ ℂ ∧ ( 𝑐 ‘ 2 ) ∈ ℂ ) )
250 1ex ⊢ 1 ∈ V
251 22 250 34 3pm3.2i ⊢ ( 0 ∈ V ∧ 1 ∈ V ∧ 2 ∈ V )
252 251 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( 0 ∈ V ∧ 1 ∈ V ∧ 2 ∈ V ) )
253 0ne1 ⊢ 0 ≠ 1
254 253 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → 0 ≠ 1 )
255 0ne2 ⊢ 0 ≠ 2
256 255 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → 0 ≠ 2 )
257 1ne2 ⊢ 1 ≠ 2
258 257 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → 1 ≠ 2 )
259 238 239 240 249 252 254 256 258 sumtp ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → Σ 𝑗 ∈ { 0 , 1 , 2 } ( 𝑐 ‘ 𝑗 ) = ( ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) + ( 𝑐 ‘ 2 ) ) )
260 232 237 259 3eqtr3rd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) + ( 𝑐 ‘ 2 ) ) = 𝑁 )
261 242 244 addcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) ∈ ℂ )
262 100 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → 𝑁 ∈ ℂ )
263 261 248 262 addrsub ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( ( ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) + ( 𝑐 ‘ 2 ) ) = 𝑁 ↔ ( 𝑐 ‘ 2 ) = ( 𝑁 − ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) ) ) )
264 260 263 mpbid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( 𝑐 ‘ 2 ) = ( 𝑁 − ( ( 𝑐 ‘ 0 ) + ( 𝑐 ‘ 1 ) ) ) )
265 231 sumeq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → Σ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑛 ‘ 𝑗 ) = Σ 𝑗 ∈ { 0 , 1 , 2 } ( 𝑛 ‘ 𝑗 ) )
266 20 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) → 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) )
267 266 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) )
268 233 234 235 267 reprsum ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → Σ 𝑗 ∈ ( 0 ..^ 3 ) ( 𝑛 ‘ 𝑗 ) = 𝑁 )
269 fveq2 ⊢ ( 𝑗 = 0 → ( 𝑛 ‘ 𝑗 ) = ( 𝑛 ‘ 0 ) )
270 fveq2 ⊢ ( 𝑗 = 1 → ( 𝑛 ‘ 𝑗 ) = ( 𝑛 ‘ 1 ) )
271 fveq2 ⊢ ( 𝑗 = 2 → ( 𝑛 ‘ 𝑗 ) = ( 𝑛 ‘ 2 ) )
272 27 nncnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝑛 ‘ 0 ) ∈ ℂ )
273 272 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) → ( 𝑛 ‘ 0 ) ∈ ℂ )
274 273 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( 𝑛 ‘ 0 ) ∈ ℂ )
275 32 nncnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝑛 ‘ 1 ) ∈ ℂ )
276 275 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) → ( 𝑛 ‘ 1 ) ∈ ℂ )
277 276 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( 𝑛 ‘ 1 ) ∈ ℂ )
278 38 nncnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝑛 ‘ 2 ) ∈ ℂ )
279 278 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) → ( 𝑛 ‘ 2 ) ∈ ℂ )
280 279 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( 𝑛 ‘ 2 ) ∈ ℂ )
281 274 277 280 3jca ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( ( 𝑛 ‘ 0 ) ∈ ℂ ∧ ( 𝑛 ‘ 1 ) ∈ ℂ ∧ ( 𝑛 ‘ 2 ) ∈ ℂ ) )
282 269 270 271 281 252 254 256 258 sumtp ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → Σ 𝑗 ∈ { 0 , 1 , 2 } ( 𝑛 ‘ 𝑗 ) = ( ( ( 𝑛 ‘ 0 ) + ( 𝑛 ‘ 1 ) ) + ( 𝑛 ‘ 2 ) ) )
283 265 268 282 3eqtr3rd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( ( ( 𝑛 ‘ 0 ) + ( 𝑛 ‘ 1 ) ) + ( 𝑛 ‘ 2 ) ) = 𝑁 )
284 274 277 addcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( ( 𝑛 ‘ 0 ) + ( 𝑛 ‘ 1 ) ) ∈ ℂ )
285 284 280 262 addrsub ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( ( ( ( 𝑛 ‘ 0 ) + ( 𝑛 ‘ 1 ) ) + ( 𝑛 ‘ 2 ) ) = 𝑁 ↔ ( 𝑛 ‘ 2 ) = ( 𝑁 − ( ( 𝑛 ‘ 0 ) + ( 𝑛 ‘ 1 ) ) ) ) )
286 283 285 mpbid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( 𝑛 ‘ 2 ) = ( 𝑁 − ( ( 𝑛 ‘ 0 ) + ( 𝑛 ‘ 1 ) ) ) )
287 230 264 286 3eqtr4d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( 𝑐 ‘ 2 ) = ( 𝑛 ‘ 2 ) )
288 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → 𝑖 = 2 )
289 288 fveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( 𝑐 ‘ 𝑖 ) = ( 𝑐 ‘ 2 ) )
290 288 fveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( 𝑛 ‘ 𝑖 ) = ( 𝑛 ‘ 2 ) )
291 287 289 290 3eqtr4d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) ∧ 𝑖 = 2 ) → ( 𝑐 ‘ 𝑖 ) = ( 𝑛 ‘ 𝑖 ) )
292 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) → 𝑖 ∈ ( 0 ..^ 3 ) )
293 292 24 eleqtrdi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) → 𝑖 ∈ { 0 , 1 , 2 } )
294 vex ⊢ 𝑖 ∈ V
295 294 eltp ⊢ ( 𝑖 ∈ { 0 , 1 , 2 } ↔ ( 𝑖 = 0 ∨ 𝑖 = 1 ∨ 𝑖 = 2 ) )
296 293 295 sylib ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) → ( 𝑖 = 0 ∨ 𝑖 = 1 ∨ 𝑖 = 2 ) )
297 220 226 291 296 mpjao3dan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) ∧ 𝑖 ∈ ( 0 ..^ 3 ) ) → ( 𝑐 ‘ 𝑖 ) = ( 𝑛 ‘ 𝑖 ) )
298 195 197 297 eqfnfvd ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) ∧ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) ) → 𝑐 = 𝑛 )
299 298 ex ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐴 ) → ( ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) → 𝑐 = 𝑛 ) )
300 299 anasss ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴 ) ) → ( ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) → 𝑐 = 𝑛 ) )
301 300 ralrimivva ⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝐴 ∀ 𝑛 ∈ 𝐴 ( ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) → 𝑐 = 𝑛 ) )
302 dff1o6 ⊢ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) : 𝐴 –1-1-onto→ ran ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ↔ ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) Fn 𝐴 ∧ ran ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) = ran ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ∧ ∀ 𝑐 ∈ 𝐴 ∀ 𝑛 ∈ 𝐴 ( ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) → 𝑐 = 𝑛 ) ) )
303 302 biimpri ⊢ ( ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) Fn 𝐴 ∧ ran ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) = ran ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ∧ ∀ 𝑐 ∈ 𝐴 ∀ 𝑛 ∈ 𝐴 ( ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑐 ) = ( ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ‘ 𝑛 ) → 𝑐 = 𝑛 ) ) → ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) : 𝐴 –1-1-onto→ ran ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) )
304 192 193 301 303 syl3anc ⊢ ( 𝜑 → ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) : 𝐴 –1-1-onto→ ran ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) )
305 180 sselda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ) → 𝑢 ∈ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) )
306 305 124 syldan ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ) → ( Λ ‘ ( 1st ‘ 𝑢 ) ) ∈ ℝ )
307 305 128 syldan ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ) → ( Λ ‘ ( 2nd ‘ 𝑢 ) ) ∈ ℝ )
308 306 307 remulcld ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ) → ( ( Λ ‘ ( 1st ‘ 𝑢 ) ) · ( Λ ‘ ( 2nd ‘ 𝑢 ) ) ) ∈ ℝ )
309 308 recnd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ) → ( ( Λ ‘ ( 1st ‘ 𝑢 ) ) · ( Λ ‘ ( 2nd ‘ 𝑢 ) ) ) ∈ ℂ )
310 188 12 304 209 309 fsumf1o ⊢ ( 𝜑 → Σ 𝑢 ∈ ran ( 𝑑 ∈ 𝐴 ↦ ⟨ ( 𝑑 ‘ 0 ) , ( 𝑑 ‘ 1 ) ⟩ ) ( ( Λ ‘ ( 1st ‘ 𝑢 ) ) · ( Λ ‘ ( 2nd ‘ 𝑢 ) ) ) = Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( Λ ‘ ( 𝑛 ‘ 1 ) ) ) )
311 75 recnd ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ∈ ℂ )
312 69 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ) → ( Λ ‘ 𝑖 ) ∈ ℂ )
313 54 311 312 fsummulc1 ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) = Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) )
314 48 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ) → ( 1 ... 𝑁 ) ∈ Fin )
315 74 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ) → ( Λ ‘ 𝑗 ) ∈ ℝ )
316 315 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( Λ ‘ 𝑗 ) ∈ ℝ )
317 316 recnd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( Λ ‘ 𝑗 ) ∈ ℂ )
318 314 312 317 fsummulc2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ) → ( ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( Λ ‘ 𝑖 ) · ( Λ ‘ 𝑗 ) ) )
319 318 sumeq2dv ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) = Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( Λ ‘ 𝑖 ) · ( Λ ‘ 𝑗 ) ) )
320 vex ⊢ 𝑗 ∈ V
321 294 320 op1std ⊢ ( 𝑢 = ⟨ 𝑖 , 𝑗 ⟩ → ( 1st ‘ 𝑢 ) = 𝑖 )
322 321 fveq2d ⊢ ( 𝑢 = ⟨ 𝑖 , 𝑗 ⟩ → ( Λ ‘ ( 1st ‘ 𝑢 ) ) = ( Λ ‘ 𝑖 ) )
323 294 320 op2ndd ⊢ ( 𝑢 = ⟨ 𝑖 , 𝑗 ⟩ → ( 2nd ‘ 𝑢 ) = 𝑗 )
324 323 fveq2d ⊢ ( 𝑢 = ⟨ 𝑖 , 𝑗 ⟩ → ( Λ ‘ ( 2nd ‘ 𝑢 ) ) = ( Λ ‘ 𝑗 ) )
325 322 324 oveq12d ⊢ ( 𝑢 = ⟨ 𝑖 , 𝑗 ⟩ → ( ( Λ ‘ ( 1st ‘ 𝑢 ) ) · ( Λ ‘ ( 2nd ‘ 𝑢 ) ) ) = ( ( Λ ‘ 𝑖 ) · ( Λ ‘ 𝑗 ) ) )
326 69 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ) → ( Λ ‘ 𝑖 ) ∈ ℝ )
327 326 315 remulcld ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ) → ( ( Λ ‘ 𝑖 ) · ( Λ ‘ 𝑗 ) ) ∈ ℝ )
328 327 recnd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ) → ( ( Λ ‘ 𝑖 ) · ( Λ ‘ 𝑗 ) ) ∈ ℂ )
329 325 54 71 328 fsumxp ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( Λ ‘ 𝑖 ) · ( Λ ‘ 𝑗 ) ) = Σ 𝑢 ∈ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) ( ( Λ ‘ ( 1st ‘ 𝑢 ) ) · ( Λ ‘ ( 2nd ‘ 𝑢 ) ) ) )
330 313 319 329 3eqtrrd ⊢ ( 𝜑 → Σ 𝑢 ∈ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) × ( 1 ... 𝑁 ) ) ( ( Λ ‘ ( 1st ‘ 𝑢 ) ) · ( Λ ‘ ( 2nd ‘ 𝑢 ) ) ) = ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) )
331 181 310 330 3brtr3d ⊢ ( 𝜑 → Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( Λ ‘ ( 𝑛 ‘ 1 ) ) ) ≤ ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) )
332 46 76 44 116 331 lemul2ad ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) · Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( Λ ‘ ( 𝑛 ‘ 1 ) ) ) ) ≤ ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) )
333 42 47 77 113 332 letrd ⊢ ( 𝜑 → Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ≤ ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) )