| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | hgt750leme.n | . . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 2 | 1 | nnnn0d 12589 | . . . . 5
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 3 |  | 3nn0 12546 | . . . . . 6
⊢ 3 ∈
ℕ0 | 
| 4 | 3 | a1i 11 | . . . . 5
⊢ (𝜑 → 3 ∈
ℕ0) | 
| 5 |  | ssidd 4006 | . . . . 5
⊢ (𝜑 → ℕ ⊆
ℕ) | 
| 6 | 2, 4, 5 | reprfi2 34639 | . . . 4
⊢ (𝜑 →
(ℕ(repr‘3)𝑁)
∈ Fin) | 
| 7 |  | hgt750lemb.a | . . . . 5
⊢ 𝐴 = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩
ℙ)} | 
| 8 | 7 | ssrab3 4081 | . . . 4
⊢ 𝐴 ⊆
(ℕ(repr‘3)𝑁) | 
| 9 |  | ssfi 9214 | . . . 4
⊢
(((ℕ(repr‘3)𝑁) ∈ Fin ∧ 𝐴 ⊆ (ℕ(repr‘3)𝑁)) → 𝐴 ∈ Fin) | 
| 10 | 6, 8, 9 | sylancl 586 | . . 3
⊢ (𝜑 → 𝐴 ∈ Fin) | 
| 11 |  | vmaf 27163 | . . . . . 6
⊢
Λ:ℕ⟶ℝ | 
| 12 | 11 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) →
Λ:ℕ⟶ℝ) | 
| 13 |  | ssidd 4006 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ℕ ⊆
ℕ) | 
| 14 | 1 | nnzd 12642 | . . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 15 | 14 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈ ℤ) | 
| 16 | 3 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 3 ∈
ℕ0) | 
| 17 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ 𝐴) | 
| 18 | 8, 17 | sselid 3980 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℕ(repr‘3)𝑁)) | 
| 19 | 13, 15, 16, 18 | reprf 34628 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛:(0..^3)⟶ℕ) | 
| 20 |  | c0ex 11256 | . . . . . . . . 9
⊢ 0 ∈
V | 
| 21 | 20 | tpid1 4767 | . . . . . . . 8
⊢ 0 ∈
{0, 1, 2} | 
| 22 |  | fzo0to3tp 13792 | . . . . . . . 8
⊢ (0..^3) =
{0, 1, 2} | 
| 23 | 21, 22 | eleqtrri 2839 | . . . . . . 7
⊢ 0 ∈
(0..^3) | 
| 24 | 23 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 0 ∈ (0..^3)) | 
| 25 | 19, 24 | ffvelcdmd 7104 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘0) ∈ ℕ) | 
| 26 | 12, 25 | ffvelcdmd 7104 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘0)) ∈ ℝ) | 
| 27 |  | 1ex 11258 | . . . . . . . . . 10
⊢ 1 ∈
V | 
| 28 | 27 | tpid2 4769 | . . . . . . . . 9
⊢ 1 ∈
{0, 1, 2} | 
| 29 | 28, 22 | eleqtrri 2839 | . . . . . . . 8
⊢ 1 ∈
(0..^3) | 
| 30 | 29 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 1 ∈ (0..^3)) | 
| 31 | 19, 30 | ffvelcdmd 7104 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘1) ∈ ℕ) | 
| 32 | 12, 31 | ffvelcdmd 7104 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘1)) ∈ ℝ) | 
| 33 |  | 2ex 12344 | . . . . . . . . . 10
⊢ 2 ∈
V | 
| 34 | 33 | tpid3 4772 | . . . . . . . . 9
⊢ 2 ∈
{0, 1, 2} | 
| 35 | 34, 22 | eleqtrri 2839 | . . . . . . . 8
⊢ 2 ∈
(0..^3) | 
| 36 | 35 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 2 ∈ (0..^3)) | 
| 37 | 19, 36 | ffvelcdmd 7104 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ∈ ℕ) | 
| 38 | 12, 37 | ffvelcdmd 7104 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘2)) ∈ ℝ) | 
| 39 | 32, 38 | remulcld 11292 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))) ∈ ℝ) | 
| 40 | 26, 39 | remulcld 11292 | . . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) ·
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈
ℝ) | 
| 41 | 10, 40 | fsumrecl 15771 | . 2
⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) ∈ ℝ) | 
| 42 | 1 | nnrpd 13076 | . . . 4
⊢ (𝜑 → 𝑁 ∈
ℝ+) | 
| 43 | 42 | relogcld 26666 | . . 3
⊢ (𝜑 → (log‘𝑁) ∈
ℝ) | 
| 44 | 26, 32 | remulcld 11292 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) ·
(Λ‘(𝑛‘1))) ∈ ℝ) | 
| 45 | 10, 44 | fsumrecl 15771 | . . 3
⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ∈
ℝ) | 
| 46 | 43, 45 | remulcld 11292 | . 2
⊢ (𝜑 → ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) ∈
ℝ) | 
| 47 |  | fzfi 14014 | . . . . . . . 8
⊢
(1...𝑁) ∈
Fin | 
| 48 |  | diffi 9216 | . . . . . . . 8
⊢
((1...𝑁) ∈ Fin
→ ((1...𝑁) ∖
ℙ) ∈ Fin) | 
| 49 | 47, 48 | ax-mp 5 | . . . . . . 7
⊢
((1...𝑁) ∖
ℙ) ∈ Fin | 
| 50 |  | snfi 9084 | . . . . . . 7
⊢ {2}
∈ Fin | 
| 51 |  | unfi 9212 | . . . . . . 7
⊢
((((1...𝑁) ∖
ℙ) ∈ Fin ∧ {2} ∈ Fin) → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈
Fin) | 
| 52 | 49, 50, 51 | mp2an 692 | . . . . . 6
⊢
(((1...𝑁) ∖
ℙ) ∪ {2}) ∈ Fin | 
| 53 | 52 | a1i 11 | . . . . 5
⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈
Fin) | 
| 54 | 11 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) →
Λ:ℕ⟶ℝ) | 
| 55 |  | difss 4135 | . . . . . . . . . 10
⊢
((1...𝑁) ∖
ℙ) ⊆ (1...𝑁) | 
| 56 | 55 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → ((1...𝑁) ∖ ℙ) ⊆ (1...𝑁)) | 
| 57 |  | 2nn 12340 | . . . . . . . . . . . 12
⊢ 2 ∈
ℕ | 
| 58 | 57 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℕ) | 
| 59 |  | hgt750lemb.2 | . . . . . . . . . . 11
⊢ (𝜑 → 2 ≤ 𝑁) | 
| 60 |  | elfz1b 13634 | . . . . . . . . . . . 12
⊢ (2 ∈
(1...𝑁) ↔ (2 ∈
ℕ ∧ 𝑁 ∈
ℕ ∧ 2 ≤ 𝑁)) | 
| 61 | 60 | biimpri 228 | . . . . . . . . . . 11
⊢ ((2
∈ ℕ ∧ 𝑁
∈ ℕ ∧ 2 ≤ 𝑁) → 2 ∈ (1...𝑁)) | 
| 62 | 58, 1, 59, 61 | syl3anc 1372 | . . . . . . . . . 10
⊢ (𝜑 → 2 ∈ (1...𝑁)) | 
| 63 | 62 | snssd 4808 | . . . . . . . . 9
⊢ (𝜑 → {2} ⊆ (1...𝑁)) | 
| 64 | 56, 63 | unssd 4191 | . . . . . . . 8
⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆
(1...𝑁)) | 
| 65 |  | fz1ssnn 13596 | . . . . . . . . 9
⊢
(1...𝑁) ⊆
ℕ | 
| 66 | 65 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → (1...𝑁) ⊆ ℕ) | 
| 67 | 64, 66 | sstrd 3993 | . . . . . . 7
⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆
ℕ) | 
| 68 | 67 | sselda 3982 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 𝑖 ∈
ℕ) | 
| 69 | 54, 68 | ffvelcdmd 7104 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) →
(Λ‘𝑖) ∈
ℝ) | 
| 70 | 53, 69 | fsumrecl 15771 | . . . 4
⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})(Λ‘𝑖)
∈ ℝ) | 
| 71 |  | fzfid 14015 | . . . . 5
⊢ (𝜑 → (1...𝑁) ∈ Fin) | 
| 72 | 11 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) →
Λ:ℕ⟶ℝ) | 
| 73 | 66 | sselda 3982 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℕ) | 
| 74 | 72, 73 | ffvelcdmd 7104 | . . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℝ) | 
| 75 | 71, 74 | fsumrecl 15771 | . . . 4
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) ∈ ℝ) | 
| 76 | 70, 75 | remulcld 11292 | . . 3
⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})(Λ‘𝑖)
· Σ𝑗 ∈
(1...𝑁)(Λ‘𝑗)) ∈ ℝ) | 
| 77 | 43, 76 | remulcld 11292 | . 2
⊢ (𝜑 → ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})(Λ‘𝑖)
· Σ𝑗 ∈
(1...𝑁)(Λ‘𝑗))) ∈ ℝ) | 
| 78 | 1 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈ ℕ) | 
| 79 | 78 | nnrpd 13076 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈
ℝ+) | 
| 80 |  | relogcl 26618 | . . . . . . 7
⊢ (𝑁 ∈ ℝ+
→ (log‘𝑁) ∈
ℝ) | 
| 81 | 79, 80 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (log‘𝑁) ∈ ℝ) | 
| 82 | 32, 81 | remulcld 11292 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘1)) ·
(log‘𝑁)) ∈
ℝ) | 
| 83 | 26, 82 | remulcld 11292 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) ·
((Λ‘(𝑛‘1)) · (log‘𝑁))) ∈
ℝ) | 
| 84 |  | vmage0 27165 | . . . . . 6
⊢ ((𝑛‘0) ∈ ℕ →
0 ≤ (Λ‘(𝑛‘0))) | 
| 85 | 25, 84 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 0 ≤ (Λ‘(𝑛‘0))) | 
| 86 |  | vmage0 27165 | . . . . . . 7
⊢ ((𝑛‘1) ∈ ℕ →
0 ≤ (Λ‘(𝑛‘1))) | 
| 87 | 31, 86 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 0 ≤ (Λ‘(𝑛‘1))) | 
| 88 | 37 | nnrpd 13076 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ∈
ℝ+) | 
| 89 | 88 | relogcld 26666 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (log‘(𝑛‘2)) ∈ ℝ) | 
| 90 |  | vmalelog 27250 | . . . . . . . 8
⊢ ((𝑛‘2) ∈ ℕ →
(Λ‘(𝑛‘2)) ≤ (log‘(𝑛‘2))) | 
| 91 | 37, 90 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘2)) ≤ (log‘(𝑛‘2))) | 
| 92 | 13, 15, 16, 18, 36 | reprle 34630 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ≤ 𝑁) | 
| 93 |  | logleb 26646 | . . . . . . . . 9
⊢ (((𝑛‘2) ∈
ℝ+ ∧ 𝑁
∈ ℝ+) → ((𝑛‘2) ≤ 𝑁 ↔ (log‘(𝑛‘2)) ≤ (log‘𝑁))) | 
| 94 | 93 | biimpa 476 | . . . . . . . 8
⊢ ((((𝑛‘2) ∈
ℝ+ ∧ 𝑁
∈ ℝ+) ∧ (𝑛‘2) ≤ 𝑁) → (log‘(𝑛‘2)) ≤ (log‘𝑁)) | 
| 95 | 88, 79, 92, 94 | syl21anc 837 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (log‘(𝑛‘2)) ≤ (log‘𝑁)) | 
| 96 | 38, 89, 81, 91, 95 | letrd 11419 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘2)) ≤ (log‘𝑁)) | 
| 97 | 38, 81, 32, 87, 96 | lemul2ad 12209 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))) ≤ ((Λ‘(𝑛‘1)) ·
(log‘𝑁))) | 
| 98 | 39, 82, 26, 85, 97 | lemul2ad 12209 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) ·
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(log‘𝑁)))) | 
| 99 | 10, 40, 83, 98 | fsumle 15836 | . . 3
⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) ≤ Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(log‘𝑁)))) | 
| 100 | 1 | nncnd 12283 | . . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 101 | 1 | nnne0d 12317 | . . . . . 6
⊢ (𝜑 → 𝑁 ≠ 0) | 
| 102 | 100, 101 | logcld 26613 | . . . . 5
⊢ (𝜑 → (log‘𝑁) ∈
ℂ) | 
| 103 | 44 | recnd 11290 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) ·
(Λ‘(𝑛‘1))) ∈ ℂ) | 
| 104 | 10, 102, 103 | fsummulc2 15821 | . . . 4
⊢ (𝜑 → ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) = Σ𝑛 ∈ 𝐴 ((log‘𝑁) · ((Λ‘(𝑛‘0)) ·
(Λ‘(𝑛‘1))))) | 
| 105 | 102 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (log‘𝑁) ∈ ℂ) | 
| 106 | 105, 103 | mulcomd 11283 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((log‘𝑁) · ((Λ‘(𝑛‘0)) ·
(Λ‘(𝑛‘1)))) = (((Λ‘(𝑛‘0)) ·
(Λ‘(𝑛‘1))) · (log‘𝑁))) | 
| 107 | 26 | recnd 11290 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘0)) ∈ ℂ) | 
| 108 | 32 | recnd 11290 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘1)) ∈ ℂ) | 
| 109 | 107, 108,
105 | mulassd 11285 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((Λ‘(𝑛‘0)) ·
(Λ‘(𝑛‘1))) · (log‘𝑁)) = ((Λ‘(𝑛‘0)) ·
((Λ‘(𝑛‘1)) · (log‘𝑁)))) | 
| 110 | 106, 109 | eqtrd 2776 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((log‘𝑁) · ((Λ‘(𝑛‘0)) ·
(Λ‘(𝑛‘1)))) = ((Λ‘(𝑛‘0)) ·
((Λ‘(𝑛‘1)) · (log‘𝑁)))) | 
| 111 | 110 | sumeq2dv 15739 | . . . 4
⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((log‘𝑁) · ((Λ‘(𝑛‘0)) ·
(Λ‘(𝑛‘1)))) = Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(log‘𝑁)))) | 
| 112 | 104, 111 | eqtr2d 2777 | . . 3
⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(log‘𝑁))) =
((log‘𝑁) ·
Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) ·
(Λ‘(𝑛‘1))))) | 
| 113 | 99, 112 | breqtrd 5168 | . 2
⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))))) | 
| 114 | 1 | nnred 12282 | . . . 4
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 115 | 1 | nnge1d 12315 | . . . 4
⊢ (𝜑 → 1 ≤ 𝑁) | 
| 116 | 114, 115 | logge0d 26673 | . . 3
⊢ (𝜑 → 0 ≤ (log‘𝑁)) | 
| 117 |  | xpfi 9359 | . . . . . 6
⊢
(((((1...𝑁) ∖
ℙ) ∪ {2}) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((((1...𝑁) ∖ ℙ) ∪ {2})
× (1...𝑁)) ∈
Fin) | 
| 118 | 53, 71, 117 | syl2anc 584 | . . . . 5
⊢ (𝜑 → ((((1...𝑁) ∖ ℙ) ∪ {2}) ×
(1...𝑁)) ∈
Fin) | 
| 119 | 11 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) ×
(1...𝑁))) →
Λ:ℕ⟶ℝ) | 
| 120 | 67 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) ×
(1...𝑁))) →
(((1...𝑁) ∖ ℙ)
∪ {2}) ⊆ ℕ) | 
| 121 |  | xp1st 8047 | . . . . . . . . 9
⊢ (𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2})
× (1...𝑁)) →
(1st ‘𝑢)
∈ (((1...𝑁) ∖
ℙ) ∪ {2})) | 
| 122 | 121 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) ×
(1...𝑁))) →
(1st ‘𝑢)
∈ (((1...𝑁) ∖
ℙ) ∪ {2})) | 
| 123 | 120, 122 | sseldd 3983 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) ×
(1...𝑁))) →
(1st ‘𝑢)
∈ ℕ) | 
| 124 | 119, 123 | ffvelcdmd 7104 | . . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) ×
(1...𝑁))) →
(Λ‘(1st ‘𝑢)) ∈ ℝ) | 
| 125 |  | xp2nd 8048 | . . . . . . . . 9
⊢ (𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2})
× (1...𝑁)) →
(2nd ‘𝑢)
∈ (1...𝑁)) | 
| 126 | 125 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) ×
(1...𝑁))) →
(2nd ‘𝑢)
∈ (1...𝑁)) | 
| 127 | 65, 126 | sselid 3980 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) ×
(1...𝑁))) →
(2nd ‘𝑢)
∈ ℕ) | 
| 128 | 119, 127 | ffvelcdmd 7104 | . . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) ×
(1...𝑁))) →
(Λ‘(2nd ‘𝑢)) ∈ ℝ) | 
| 129 | 124, 128 | remulcld 11292 | . . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) ×
(1...𝑁))) →
((Λ‘(1st ‘𝑢)) · (Λ‘(2nd
‘𝑢))) ∈
ℝ) | 
| 130 |  | vmage0 27165 | . . . . . . 7
⊢
((1st ‘𝑢) ∈ ℕ → 0 ≤
(Λ‘(1st ‘𝑢))) | 
| 131 | 123, 130 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) ×
(1...𝑁))) → 0 ≤
(Λ‘(1st ‘𝑢))) | 
| 132 |  | vmage0 27165 | . . . . . . 7
⊢
((2nd ‘𝑢) ∈ ℕ → 0 ≤
(Λ‘(2nd ‘𝑢))) | 
| 133 | 127, 132 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) ×
(1...𝑁))) → 0 ≤
(Λ‘(2nd ‘𝑢))) | 
| 134 | 124, 128,
131, 133 | mulge0d 11841 | . . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) ×
(1...𝑁))) → 0 ≤
((Λ‘(1st ‘𝑢)) · (Λ‘(2nd
‘𝑢)))) | 
| 135 |  | ssidd 4006 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ℕ ⊆
ℕ) | 
| 136 | 14 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑁 ∈ ℤ) | 
| 137 | 3 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 3 ∈
ℕ0) | 
| 138 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ 𝐴) | 
| 139 | 8, 138 | sselid 3980 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ (ℕ(repr‘3)𝑁)) | 
| 140 | 135, 136,
137, 139 | reprf 34628 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐:(0..^3)⟶ℕ) | 
| 141 | 23 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 0 ∈ (0..^3)) | 
| 142 | 140, 141 | ffvelcdmd 7104 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ ℕ) | 
| 143 | 1 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑁 ∈ ℕ) | 
| 144 | 135, 136,
137, 139, 141 | reprle 34630 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ≤ 𝑁) | 
| 145 |  | elfz1b 13634 | . . . . . . . . . . . . 13
⊢ ((𝑐‘0) ∈ (1...𝑁) ↔ ((𝑐‘0) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘0) ≤ 𝑁)) | 
| 146 | 145 | biimpri 228 | . . . . . . . . . . . 12
⊢ (((𝑐‘0) ∈ ℕ ∧
𝑁 ∈ ℕ ∧
(𝑐‘0) ≤ 𝑁) → (𝑐‘0) ∈ (1...𝑁)) | 
| 147 | 142, 143,
144, 146 | syl3anc 1372 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ (1...𝑁)) | 
| 148 | 7 | reqabi 3459 | . . . . . . . . . . . . . 14
⊢ (𝑐 ∈ 𝐴 ↔ (𝑐 ∈ (ℕ(repr‘3)𝑁) ∧ ¬ (𝑐‘0) ∈ (𝑂 ∩
ℙ))) | 
| 149 | 148 | simprbi 496 | . . . . . . . . . . . . 13
⊢ (𝑐 ∈ 𝐴 → ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)) | 
| 150 |  | hgt750leme.o | . . . . . . . . . . . . . . 15
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧} | 
| 151 | 150 | oddprm2 34671 | . . . . . . . . . . . . . 14
⊢ (ℙ
∖ {2}) = (𝑂 ∩
ℙ) | 
| 152 | 151 | eleq2i 2832 | . . . . . . . . . . . . 13
⊢ ((𝑐‘0) ∈ (ℙ
∖ {2}) ↔ (𝑐‘0) ∈ (𝑂 ∩ ℙ)) | 
| 153 | 149, 152 | sylnibr 329 | . . . . . . . . . . . 12
⊢ (𝑐 ∈ 𝐴 → ¬ (𝑐‘0) ∈ (ℙ ∖
{2})) | 
| 154 | 138, 153 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ¬ (𝑐‘0) ∈ (ℙ ∖
{2})) | 
| 155 | 147, 154 | jca 511 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑐‘0) ∈ (1...𝑁) ∧ ¬ (𝑐‘0) ∈ (ℙ ∖
{2}))) | 
| 156 |  | eldif 3960 | . . . . . . . . . 10
⊢ ((𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖ {2}))
↔ ((𝑐‘0) ∈
(1...𝑁) ∧ ¬ (𝑐‘0) ∈ (ℙ
∖ {2}))) | 
| 157 | 155, 156 | sylibr 234 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖
{2}))) | 
| 158 |  | uncom 4157 | . . . . . . . . . . . . 13
⊢
(((1...𝑁) ∖
ℙ) ∪ {2}) = ({2} ∪ ((1...𝑁) ∖ ℙ)) | 
| 159 |  | undif3 4299 | . . . . . . . . . . . . 13
⊢ ({2}
∪ ((1...𝑁) ∖
ℙ)) = (({2} ∪ (1...𝑁)) ∖ (ℙ ∖
{2})) | 
| 160 | 158, 159 | eqtri 2764 | . . . . . . . . . . . 12
⊢
(((1...𝑁) ∖
ℙ) ∪ {2}) = (({2} ∪ (1...𝑁)) ∖ (ℙ ∖
{2})) | 
| 161 |  | ssequn1 4185 | . . . . . . . . . . . . . 14
⊢ ({2}
⊆ (1...𝑁) ↔ ({2}
∪ (1...𝑁)) = (1...𝑁)) | 
| 162 | 63, 161 | sylib 218 | . . . . . . . . . . . . 13
⊢ (𝜑 → ({2} ∪ (1...𝑁)) = (1...𝑁)) | 
| 163 | 162 | difeq1d 4124 | . . . . . . . . . . . 12
⊢ (𝜑 → (({2} ∪ (1...𝑁)) ∖ (ℙ ∖
{2})) = ((1...𝑁) ∖
(ℙ ∖ {2}))) | 
| 164 | 160, 163 | eqtrid 2788 | . . . . . . . . . . 11
⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) = ((1...𝑁) ∖ (ℙ ∖
{2}))) | 
| 165 | 164 | eleq2d 2826 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑐‘0) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ↔ (𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖
{2})))) | 
| 166 | 165 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑐‘0) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ↔ (𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖
{2})))) | 
| 167 | 157, 166 | mpbird 257 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ (((1...𝑁) ∖ ℙ) ∪
{2})) | 
| 168 | 29 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 ∈ (0..^3)) | 
| 169 | 140, 168 | ffvelcdmd 7104 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ∈ ℕ) | 
| 170 | 135, 136,
137, 139, 168 | reprle 34630 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ≤ 𝑁) | 
| 171 |  | elfz1b 13634 | . . . . . . . . . 10
⊢ ((𝑐‘1) ∈ (1...𝑁) ↔ ((𝑐‘1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘1) ≤ 𝑁)) | 
| 172 | 171 | biimpri 228 | . . . . . . . . 9
⊢ (((𝑐‘1) ∈ ℕ ∧
𝑁 ∈ ℕ ∧
(𝑐‘1) ≤ 𝑁) → (𝑐‘1) ∈ (1...𝑁)) | 
| 173 | 169, 143,
170, 172 | syl3anc 1372 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ∈ (1...𝑁)) | 
| 174 | 167, 173 | opelxpd 5723 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 〈(𝑐‘0), (𝑐‘1)〉 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2})
× (1...𝑁))) | 
| 175 | 174 | ralrimiva 3145 | . . . . . 6
⊢ (𝜑 → ∀𝑐 ∈ 𝐴 〈(𝑐‘0), (𝑐‘1)〉 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2})
× (1...𝑁))) | 
| 176 |  | fveq1 6904 | . . . . . . . . 9
⊢ (𝑑 = 𝑐 → (𝑑‘0) = (𝑐‘0)) | 
| 177 |  | fveq1 6904 | . . . . . . . . 9
⊢ (𝑑 = 𝑐 → (𝑑‘1) = (𝑐‘1)) | 
| 178 | 176, 177 | opeq12d 4880 | . . . . . . . 8
⊢ (𝑑 = 𝑐 → 〈(𝑑‘0), (𝑑‘1)〉 = 〈(𝑐‘0), (𝑐‘1)〉) | 
| 179 | 178 | cbvmptv 5254 | . . . . . . 7
⊢ (𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉) = (𝑐 ∈ 𝐴 ↦ 〈(𝑐‘0), (𝑐‘1)〉) | 
| 180 | 179 | rnmptss 7142 | . . . . . 6
⊢
(∀𝑐 ∈
𝐴 〈(𝑐‘0), (𝑐‘1)〉 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2})
× (1...𝑁)) → ran
(𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉) ⊆ ((((1...𝑁) ∖ ℙ) ∪ {2})
× (1...𝑁))) | 
| 181 | 175, 180 | syl 17 | . . . . 5
⊢ (𝜑 → ran (𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉) ⊆ ((((1...𝑁) ∖ ℙ) ∪ {2})
× (1...𝑁))) | 
| 182 | 118, 129,
134, 181 | fsumless 15833 | . . . 4
⊢ (𝜑 → Σ𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)((Λ‘(1st
‘𝑢)) ·
(Λ‘(2nd ‘𝑢))) ≤ Σ𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) ×
(1...𝑁))((Λ‘(1st ‘𝑢)) ·
(Λ‘(2nd ‘𝑢)))) | 
| 183 |  | fvex 6918 | . . . . . . . 8
⊢ (𝑛‘0) ∈
V | 
| 184 |  | fvex 6918 | . . . . . . . 8
⊢ (𝑛‘1) ∈
V | 
| 185 | 183, 184 | op1std 8025 | . . . . . . 7
⊢ (𝑢 = 〈(𝑛‘0), (𝑛‘1)〉 → (1st
‘𝑢) = (𝑛‘0)) | 
| 186 | 185 | fveq2d 6909 | . . . . . 6
⊢ (𝑢 = 〈(𝑛‘0), (𝑛‘1)〉 →
(Λ‘(1st ‘𝑢)) = (Λ‘(𝑛‘0))) | 
| 187 | 183, 184 | op2ndd 8026 | . . . . . . 7
⊢ (𝑢 = 〈(𝑛‘0), (𝑛‘1)〉 → (2nd
‘𝑢) = (𝑛‘1)) | 
| 188 | 187 | fveq2d 6909 | . . . . . 6
⊢ (𝑢 = 〈(𝑛‘0), (𝑛‘1)〉 →
(Λ‘(2nd ‘𝑢)) = (Λ‘(𝑛‘1))) | 
| 189 | 186, 188 | oveq12d 7450 | . . . . 5
⊢ (𝑢 = 〈(𝑛‘0), (𝑛‘1)〉 →
((Λ‘(1st ‘𝑢)) · (Λ‘(2nd
‘𝑢))) =
((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) | 
| 190 |  | opex 5468 | . . . . . . . 8
⊢
〈(𝑐‘0),
(𝑐‘1)〉 ∈
V | 
| 191 | 190 | rgenw 3064 | . . . . . . 7
⊢
∀𝑐 ∈
𝐴 〈(𝑐‘0), (𝑐‘1)〉 ∈ V | 
| 192 | 179 | fnmpt 6707 | . . . . . . 7
⊢
(∀𝑐 ∈
𝐴 〈(𝑐‘0), (𝑐‘1)〉 ∈ V → (𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉) Fn 𝐴) | 
| 193 | 191, 192 | mp1i 13 | . . . . . 6
⊢ (𝜑 → (𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉) Fn 𝐴) | 
| 194 |  | eqidd 2737 | . . . . . 6
⊢ (𝜑 → ran (𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉) = ran (𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)) | 
| 195 | 140 | ad2antrr 726 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) → 𝑐:(0..^3)⟶ℕ) | 
| 196 | 195 | ffnd 6736 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) → 𝑐 Fn (0..^3)) | 
| 197 | 19 | ad4ant13 751 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) → 𝑛:(0..^3)⟶ℕ) | 
| 198 | 197 | ffnd 6736 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) → 𝑛 Fn (0..^3)) | 
| 199 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) → ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) | 
| 200 | 179 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉) = (𝑐 ∈ 𝐴 ↦ 〈(𝑐‘0), (𝑐‘1)〉)) | 
| 201 | 190 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 〈(𝑐‘0), (𝑐‘1)〉 ∈ V) | 
| 202 | 200, 201 | fvmpt2d 7028 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = 〈(𝑐‘0), (𝑐‘1)〉) | 
| 203 | 202 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = 〈(𝑐‘0), (𝑐‘1)〉) | 
| 204 | 203 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) → ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = 〈(𝑐‘0), (𝑐‘1)〉) | 
| 205 |  | fveq1 6904 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 = 𝑛 → (𝑐‘0) = (𝑛‘0)) | 
| 206 |  | fveq1 6904 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 = 𝑛 → (𝑐‘1) = (𝑛‘1)) | 
| 207 | 205, 206 | opeq12d 4880 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 = 𝑛 → 〈(𝑐‘0), (𝑐‘1)〉 = 〈(𝑛‘0), (𝑛‘1)〉) | 
| 208 |  | opex 5468 | . . . . . . . . . . . . . . . . . . . 20
⊢
〈(𝑛‘0),
(𝑛‘1)〉 ∈
V | 
| 209 | 208 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 〈(𝑛‘0), (𝑛‘1)〉 ∈ V) | 
| 210 | 179, 207,
17, 209 | fvmptd3 7038 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛) = 〈(𝑛‘0), (𝑛‘1)〉) | 
| 211 | 210 | adantlr 715 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛) = 〈(𝑛‘0), (𝑛‘1)〉) | 
| 212 | 211 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) → ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛) = 〈(𝑛‘0), (𝑛‘1)〉) | 
| 213 | 199, 204,
212 | 3eqtr3d 2784 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) → 〈(𝑐‘0), (𝑐‘1)〉 = 〈(𝑛‘0), (𝑛‘1)〉) | 
| 214 | 183, 184 | opth2 5484 | . . . . . . . . . . . . . . 15
⊢
(〈(𝑐‘0),
(𝑐‘1)〉 =
〈(𝑛‘0), (𝑛‘1)〉 ↔ ((𝑐‘0) = (𝑛‘0) ∧ (𝑐‘1) = (𝑛‘1))) | 
| 215 | 213, 214 | sylib 218 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) → ((𝑐‘0) = (𝑛‘0) ∧ (𝑐‘1) = (𝑛‘1))) | 
| 216 | 215 | simpld 494 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) → (𝑐‘0) = (𝑛‘0)) | 
| 217 | 216 | ad2antrr 726 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑐‘0) = (𝑛‘0)) | 
| 218 |  | simpr 484 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → 𝑖 = 0) | 
| 219 | 218 | fveq2d 6909 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑐‘𝑖) = (𝑐‘0)) | 
| 220 | 218 | fveq2d 6909 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑛‘𝑖) = (𝑛‘0)) | 
| 221 | 217, 219,
220 | 3eqtr4d 2786 | . . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑐‘𝑖) = (𝑛‘𝑖)) | 
| 222 | 215 | simprd 495 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) → (𝑐‘1) = (𝑛‘1)) | 
| 223 | 222 | ad2antrr 726 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑐‘1) = (𝑛‘1)) | 
| 224 |  | simpr 484 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → 𝑖 = 1) | 
| 225 | 224 | fveq2d 6909 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑐‘𝑖) = (𝑐‘1)) | 
| 226 | 224 | fveq2d 6909 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑛‘𝑖) = (𝑛‘1)) | 
| 227 | 223, 225,
226 | 3eqtr4d 2786 | . . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑐‘𝑖) = (𝑛‘𝑖)) | 
| 228 | 216 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘0) = (𝑛‘0)) | 
| 229 | 222 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘1) = (𝑛‘1)) | 
| 230 | 228, 229 | oveq12d 7450 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑐‘0) + (𝑐‘1)) = ((𝑛‘0) + (𝑛‘1))) | 
| 231 | 230 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑁 − ((𝑐‘0) + (𝑐‘1))) = (𝑁 − ((𝑛‘0) + (𝑛‘1)))) | 
| 232 | 22 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (0..^3) = {0, 1,
2}) | 
| 233 | 232 | sumeq1d 15737 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑐‘𝑗) = Σ𝑗 ∈ {0, 1, 2} (𝑐‘𝑗)) | 
| 234 |  | ssidd 4006 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ℕ ⊆
ℕ) | 
| 235 | 136 | ad4antr 732 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑁 ∈ ℤ) | 
| 236 | 3 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 3 ∈
ℕ0) | 
| 237 | 139 | ad4antr 732 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑐 ∈ (ℕ(repr‘3)𝑁)) | 
| 238 | 234, 235,
236, 237 | reprsum 34629 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑐‘𝑗) = 𝑁) | 
| 239 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 = 0 → (𝑐‘𝑗) = (𝑐‘0)) | 
| 240 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 = 1 → (𝑐‘𝑗) = (𝑐‘1)) | 
| 241 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 = 2 → (𝑐‘𝑗) = (𝑐‘2)) | 
| 242 | 142 | nncnd 12283 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ ℂ) | 
| 243 | 242 | ad4antr 732 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘0) ∈ ℂ) | 
| 244 | 169 | nncnd 12283 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ∈ ℂ) | 
| 245 | 244 | ad4antr 732 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘1) ∈ ℂ) | 
| 246 | 35 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 2 ∈ (0..^3)) | 
| 247 | 140, 246 | ffvelcdmd 7104 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘2) ∈ ℕ) | 
| 248 | 247 | nncnd 12283 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘2) ∈ ℂ) | 
| 249 | 248 | ad4antr 732 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘2) ∈ ℂ) | 
| 250 | 243, 245,
249 | 3jca 1128 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑐‘0) ∈ ℂ ∧ (𝑐‘1) ∈ ℂ ∧
(𝑐‘2) ∈
ℂ)) | 
| 251 | 20, 27, 33 | 3pm3.2i 1339 | . . . . . . . . . . . . . . . . 17
⊢ (0 ∈
V ∧ 1 ∈ V ∧ 2 ∈ V) | 
| 252 | 251 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (0 ∈ V ∧ 1 ∈ V
∧ 2 ∈ V)) | 
| 253 |  | 0ne1 12338 | . . . . . . . . . . . . . . . . 17
⊢ 0 ≠
1 | 
| 254 | 253 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 0 ≠ 1) | 
| 255 |  | 0ne2 12474 | . . . . . . . . . . . . . . . . 17
⊢ 0 ≠
2 | 
| 256 | 255 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 0 ≠ 2) | 
| 257 |  | 1ne2 12475 | . . . . . . . . . . . . . . . . 17
⊢ 1 ≠
2 | 
| 258 | 257 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 1 ≠ 2) | 
| 259 | 239, 240,
241, 250, 252, 254, 256, 258 | sumtp 15786 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ {0, 1, 2} (𝑐‘𝑗) = (((𝑐‘0) + (𝑐‘1)) + (𝑐‘2))) | 
| 260 | 233, 238,
259 | 3eqtr3rd 2785 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (((𝑐‘0) + (𝑐‘1)) + (𝑐‘2)) = 𝑁) | 
| 261 | 243, 245 | addcld 11281 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑐‘0) + (𝑐‘1)) ∈ ℂ) | 
| 262 | 100 | ad5antr 734 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑁 ∈ ℂ) | 
| 263 | 261, 249,
262 | addrsub 11681 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((((𝑐‘0) + (𝑐‘1)) + (𝑐‘2)) = 𝑁 ↔ (𝑐‘2) = (𝑁 − ((𝑐‘0) + (𝑐‘1))))) | 
| 264 | 260, 263 | mpbid 232 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘2) = (𝑁 − ((𝑐‘0) + (𝑐‘1)))) | 
| 265 | 232 | sumeq1d 15737 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑛‘𝑗) = Σ𝑗 ∈ {0, 1, 2} (𝑛‘𝑗)) | 
| 266 | 18 | ad4ant13 751 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) → 𝑛 ∈ (ℕ(repr‘3)𝑁)) | 
| 267 | 266 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑛 ∈ (ℕ(repr‘3)𝑁)) | 
| 268 | 234, 235,
236, 267 | reprsum 34629 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑛‘𝑗) = 𝑁) | 
| 269 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 = 0 → (𝑛‘𝑗) = (𝑛‘0)) | 
| 270 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 = 1 → (𝑛‘𝑗) = (𝑛‘1)) | 
| 271 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 = 2 → (𝑛‘𝑗) = (𝑛‘2)) | 
| 272 | 25 | nncnd 12283 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘0) ∈ ℂ) | 
| 273 | 272 | adantlr 715 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → (𝑛‘0) ∈ ℂ) | 
| 274 | 273 | ad3antrrr 730 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘0) ∈ ℂ) | 
| 275 | 31 | nncnd 12283 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘1) ∈ ℂ) | 
| 276 | 275 | adantlr 715 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → (𝑛‘1) ∈ ℂ) | 
| 277 | 276 | ad3antrrr 730 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘1) ∈ ℂ) | 
| 278 | 37 | nncnd 12283 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ∈ ℂ) | 
| 279 | 278 | adantlr 715 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ∈ ℂ) | 
| 280 | 279 | ad3antrrr 730 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘2) ∈ ℂ) | 
| 281 | 274, 277,
280 | 3jca 1128 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑛‘0) ∈ ℂ ∧ (𝑛‘1) ∈ ℂ ∧
(𝑛‘2) ∈
ℂ)) | 
| 282 | 269, 270,
271, 281, 252, 254, 256, 258 | sumtp 15786 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ {0, 1, 2} (𝑛‘𝑗) = (((𝑛‘0) + (𝑛‘1)) + (𝑛‘2))) | 
| 283 | 265, 268,
282 | 3eqtr3rd 2785 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (((𝑛‘0) + (𝑛‘1)) + (𝑛‘2)) = 𝑁) | 
| 284 | 274, 277 | addcld 11281 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑛‘0) + (𝑛‘1)) ∈ ℂ) | 
| 285 | 284, 280,
262 | addrsub 11681 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((((𝑛‘0) + (𝑛‘1)) + (𝑛‘2)) = 𝑁 ↔ (𝑛‘2) = (𝑁 − ((𝑛‘0) + (𝑛‘1))))) | 
| 286 | 283, 285 | mpbid 232 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘2) = (𝑁 − ((𝑛‘0) + (𝑛‘1)))) | 
| 287 | 231, 264,
286 | 3eqtr4d 2786 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘2) = (𝑛‘2)) | 
| 288 |  | simpr 484 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑖 = 2) | 
| 289 | 288 | fveq2d 6909 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘𝑖) = (𝑐‘2)) | 
| 290 | 288 | fveq2d 6909 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘𝑖) = (𝑛‘2)) | 
| 291 | 287, 289,
290 | 3eqtr4d 2786 | . . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘𝑖) = (𝑛‘𝑖)) | 
| 292 |  | simpr 484 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → 𝑖 ∈ (0..^3)) | 
| 293 | 292, 22 | eleqtrdi 2850 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → 𝑖 ∈ {0, 1, 2}) | 
| 294 |  | vex 3483 | . . . . . . . . . . . . 13
⊢ 𝑖 ∈ V | 
| 295 | 294 | eltp 4688 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ {0, 1, 2} ↔ (𝑖 = 0 ∨ 𝑖 = 1 ∨ 𝑖 = 2)) | 
| 296 | 293, 295 | sylib 218 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → (𝑖 = 0 ∨ 𝑖 = 1 ∨ 𝑖 = 2)) | 
| 297 | 221, 227,
291, 296 | mpjao3dan 1433 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → (𝑐‘𝑖) = (𝑛‘𝑖)) | 
| 298 | 196, 198,
297 | eqfnfvd 7053 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛)) → 𝑐 = 𝑛) | 
| 299 | 298 | ex 412 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → (((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛) → 𝑐 = 𝑛)) | 
| 300 | 299 | anasss 466 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴)) → (((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛) → 𝑐 = 𝑛)) | 
| 301 | 300 | ralrimivva 3201 | . . . . . 6
⊢ (𝜑 → ∀𝑐 ∈ 𝐴 ∀𝑛 ∈ 𝐴 (((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛) → 𝑐 = 𝑛)) | 
| 302 |  | dff1o6 7296 | . . . . . . 7
⊢ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉):𝐴–1-1-onto→ran
(𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉) ↔ ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉) Fn 𝐴 ∧ ran (𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉) = ran (𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉) ∧ ∀𝑐 ∈ 𝐴 ∀𝑛 ∈ 𝐴 (((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)‘𝑛) → 𝑐 = 𝑛))) | 
| 303 | 302 | biimpri 228 | . . . . . 6
⊢ (((𝑑 ∈ 𝐴 ↦ 〈(𝑑‘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 1372 | . . . . 5
⊢ (𝜑 → (𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉):𝐴–1-1-onto→ran
(𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)) | 
| 305 | 181 | sselda 3982 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)) → 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) ×
(1...𝑁))) | 
| 306 | 305, 124 | syldan 591 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)) →
(Λ‘(1st ‘𝑢)) ∈ ℝ) | 
| 307 | 305, 128 | syldan 591 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)) →
(Λ‘(2nd ‘𝑢)) ∈ ℝ) | 
| 308 | 306, 307 | remulcld 11292 | . . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)) →
((Λ‘(1st ‘𝑢)) · (Λ‘(2nd
‘𝑢))) ∈
ℝ) | 
| 309 | 308 | recnd 11290 | . . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)) →
((Λ‘(1st ‘𝑢)) · (Λ‘(2nd
‘𝑢))) ∈
ℂ) | 
| 310 | 189, 10, 304, 210, 309 | fsumf1o 15760 | . . . 4
⊢ (𝜑 → Σ𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ 〈(𝑑‘0), (𝑑‘1)〉)((Λ‘(1st
‘𝑢)) ·
(Λ‘(2nd ‘𝑢))) = Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) | 
| 311 | 75 | recnd 11290 | . . . . . 6
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) ∈ ℂ) | 
| 312 | 69 | recnd 11290 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) →
(Λ‘𝑖) ∈
ℂ) | 
| 313 | 53, 311, 312 | fsummulc1 15822 | . . . . 5
⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})(Λ‘𝑖)
· Σ𝑗 ∈
(1...𝑁)(Λ‘𝑗)) = Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})((Λ‘𝑖)
· Σ𝑗 ∈
(1...𝑁)(Λ‘𝑗))) | 
| 314 | 47 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) →
(1...𝑁) ∈
Fin) | 
| 315 | 74 | adantrl 716 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → (Λ‘𝑗) ∈
ℝ) | 
| 316 | 315 | anassrs 467 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℝ) | 
| 317 | 316 | recnd 11290 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℂ) | 
| 318 | 314, 312,
317 | fsummulc2 15821 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) →
((Λ‘𝑖)
· Σ𝑗 ∈
(1...𝑁)(Λ‘𝑗)) = Σ𝑗 ∈ (1...𝑁)((Λ‘𝑖) · (Λ‘𝑗))) | 
| 319 | 318 | sumeq2dv 15739 | . . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})((Λ‘𝑖)
· Σ𝑗 ∈
(1...𝑁)(Λ‘𝑗)) = Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})Σ𝑗 ∈ (1...𝑁)((Λ‘𝑖) · (Λ‘𝑗))) | 
| 320 |  | vex 3483 | . . . . . . . . 9
⊢ 𝑗 ∈ V | 
| 321 | 294, 320 | op1std 8025 | . . . . . . . 8
⊢ (𝑢 = 〈𝑖, 𝑗〉 → (1st ‘𝑢) = 𝑖) | 
| 322 | 321 | fveq2d 6909 | . . . . . . 7
⊢ (𝑢 = 〈𝑖, 𝑗〉 → (Λ‘(1st
‘𝑢)) =
(Λ‘𝑖)) | 
| 323 | 294, 320 | op2ndd 8026 | . . . . . . . 8
⊢ (𝑢 = 〈𝑖, 𝑗〉 → (2nd ‘𝑢) = 𝑗) | 
| 324 | 323 | fveq2d 6909 | . . . . . . 7
⊢ (𝑢 = 〈𝑖, 𝑗〉 → (Λ‘(2nd
‘𝑢)) =
(Λ‘𝑗)) | 
| 325 | 322, 324 | oveq12d 7450 | . . . . . 6
⊢ (𝑢 = 〈𝑖, 𝑗〉 →
((Λ‘(1st ‘𝑢)) · (Λ‘(2nd
‘𝑢))) =
((Λ‘𝑖)
· (Λ‘𝑗))) | 
| 326 | 69 | adantrr 717 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → (Λ‘𝑖) ∈
ℝ) | 
| 327 | 326, 315 | remulcld 11292 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → ((Λ‘𝑖) · (Λ‘𝑗)) ∈
ℝ) | 
| 328 | 327 | recnd 11290 | . . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → ((Λ‘𝑖) · (Λ‘𝑗)) ∈
ℂ) | 
| 329 | 325, 53, 71, 328 | fsumxp 15809 | . . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})Σ𝑗 ∈ (1...𝑁)((Λ‘𝑖) · (Λ‘𝑗)) = Σ𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) ×
(1...𝑁))((Λ‘(1st
‘𝑢)) ·
(Λ‘(2nd ‘𝑢)))) | 
| 330 | 313, 319,
329 | 3eqtrrd 2781 | . . . 4
⊢ (𝜑 → Σ𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) ×
(1...𝑁))((Λ‘(1st
‘𝑢)) ·
(Λ‘(2nd ‘𝑢))) = (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})(Λ‘𝑖)
· Σ𝑗 ∈
(1...𝑁)(Λ‘𝑗))) | 
| 331 | 182, 310,
330 | 3brtr3d 5173 | . . 3
⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ≤ (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})(Λ‘𝑖)
· Σ𝑗 ∈
(1...𝑁)(Λ‘𝑗))) | 
| 332 | 45, 76, 43, 116, 331 | lemul2ad 12209 | . 2
⊢ (𝜑 → ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) ≤
((log‘𝑁) ·
(Σ𝑖 ∈
(((1...𝑁) ∖ ℙ)
∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) | 
| 333 | 41, 46, 77, 113, 332 | letrd 11419 | 1
⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})(Λ‘𝑖)
· Σ𝑗 ∈
(1...𝑁)(Λ‘𝑗)))) |