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