Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hgt750lemb Structured version   Visualization version   GIF version

Theorem hgt750lemb 30862
 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.)
Hypotheses
Ref Expression
hgt750leme.o 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
hgt750leme.n (𝜑𝑁 ∈ ℕ)
hgt750lemb.2 (𝜑 → 2 ≤ 𝑁)
hgt750lemb.a 𝐴 = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
Assertion
Ref Expression
hgt750lemb (𝜑 → Σ𝑛𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))
Distinct variable groups:   𝑧,𝑂   𝐴,𝑐,𝑖,𝑗,𝑛   𝑁,𝑐,𝑖,𝑗,𝑛   𝜑,𝑐,𝑖,𝑗,𝑛
Allowed substitution hints:   𝜑(𝑧)   𝐴(𝑧)   𝑁(𝑧)   𝑂(𝑖,𝑗,𝑛,𝑐)

Proof of Theorem hgt750lemb
Dummy variables 𝑑 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hgt750leme.n . . . . . 6 (𝜑𝑁 ∈ ℕ)
21nnnn0d 11389 . . . . 5 (𝜑𝑁 ∈ ℕ0)
3 3nn0 11348 . . . . . 6 3 ∈ ℕ0
43a1i 11 . . . . 5 (𝜑 → 3 ∈ ℕ0)
5 ssid 3657 . . . . . 6 ℕ ⊆ ℕ
65a1i 11 . . . . 5 (𝜑 → ℕ ⊆ ℕ)
72, 4, 6reprfi2 30829 . . . 4 (𝜑 → (ℕ(repr‘3)𝑁) ∈ Fin)
8 hgt750lemb.a . . . . 5 𝐴 = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
98ssrab3 3721 . . . 4 𝐴 ⊆ (ℕ(repr‘3)𝑁)
10 ssfi 8221 . . . 4 (((ℕ(repr‘3)𝑁) ∈ Fin ∧ 𝐴 ⊆ (ℕ(repr‘3)𝑁)) → 𝐴 ∈ Fin)
117, 9, 10sylancl 695 . . 3 (𝜑𝐴 ∈ Fin)
12 vmaf 24890 . . . . . 6 Λ:ℕ⟶ℝ
1312a1i 11 . . . . 5 ((𝜑𝑛𝐴) → Λ:ℕ⟶ℝ)
145a1i 11 . . . . . . 7 ((𝜑𝑛𝐴) → ℕ ⊆ ℕ)
151nnzd 11519 . . . . . . . 8 (𝜑𝑁 ∈ ℤ)
1615adantr 480 . . . . . . 7 ((𝜑𝑛𝐴) → 𝑁 ∈ ℤ)
173a1i 11 . . . . . . 7 ((𝜑𝑛𝐴) → 3 ∈ ℕ0)
18 simpr 476 . . . . . . . 8 ((𝜑𝑛𝐴) → 𝑛𝐴)
199, 18sseldi 3634 . . . . . . 7 ((𝜑𝑛𝐴) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
2014, 16, 17, 19reprf 30818 . . . . . 6 ((𝜑𝑛𝐴) → 𝑛:(0..^3)⟶ℕ)
21 c0ex 10072 . . . . . . . . 9 0 ∈ V
2221tpid1 4335 . . . . . . . 8 0 ∈ {0, 1, 2}
23 fzo0to3tp 12594 . . . . . . . 8 (0..^3) = {0, 1, 2}
2422, 23eleqtrri 2729 . . . . . . 7 0 ∈ (0..^3)
2524a1i 11 . . . . . 6 ((𝜑𝑛𝐴) → 0 ∈ (0..^3))
2620, 25ffvelrnd 6400 . . . . 5 ((𝜑𝑛𝐴) → (𝑛‘0) ∈ ℕ)
2713, 26ffvelrnd 6400 . . . 4 ((𝜑𝑛𝐴) → (Λ‘(𝑛‘0)) ∈ ℝ)
28 1ex 10073 . . . . . . . . . 10 1 ∈ V
2928tpid2 4336 . . . . . . . . 9 1 ∈ {0, 1, 2}
3029, 23eleqtrri 2729 . . . . . . . 8 1 ∈ (0..^3)
3130a1i 11 . . . . . . 7 ((𝜑𝑛𝐴) → 1 ∈ (0..^3))
3220, 31ffvelrnd 6400 . . . . . 6 ((𝜑𝑛𝐴) → (𝑛‘1) ∈ ℕ)
3313, 32ffvelrnd 6400 . . . . 5 ((𝜑𝑛𝐴) → (Λ‘(𝑛‘1)) ∈ ℝ)
34 2ex 11130 . . . . . . . . . 10 2 ∈ V
3534tpid3 4338 . . . . . . . . 9 2 ∈ {0, 1, 2}
3635, 23eleqtrri 2729 . . . . . . . 8 2 ∈ (0..^3)
3736a1i 11 . . . . . . 7 ((𝜑𝑛𝐴) → 2 ∈ (0..^3))
3820, 37ffvelrnd 6400 . . . . . 6 ((𝜑𝑛𝐴) → (𝑛‘2) ∈ ℕ)
3913, 38ffvelrnd 6400 . . . . 5 ((𝜑𝑛𝐴) → (Λ‘(𝑛‘2)) ∈ ℝ)
4033, 39remulcld 10108 . . . 4 ((𝜑𝑛𝐴) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈ ℝ)
4127, 40remulcld 10108 . . 3 ((𝜑𝑛𝐴) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
4211, 41fsumrecl 14509 . 2 (𝜑 → Σ𝑛𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
431nnrpd 11908 . . . 4 (𝜑𝑁 ∈ ℝ+)
4443relogcld 24414 . . 3 (𝜑 → (log‘𝑁) ∈ ℝ)
4527, 33remulcld 10108 . . . 4 ((𝜑𝑛𝐴) → ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ∈ ℝ)
4611, 45fsumrecl 14509 . . 3 (𝜑 → Σ𝑛𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ∈ ℝ)
4744, 46remulcld 10108 . 2 (𝜑 → ((log‘𝑁) · Σ𝑛𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) ∈ ℝ)
48 fzfi 12811 . . . . . . . 8 (1...𝑁) ∈ Fin
49 diffi 8233 . . . . . . . 8 ((1...𝑁) ∈ Fin → ((1...𝑁) ∖ ℙ) ∈ Fin)
5048, 49ax-mp 5 . . . . . . 7 ((1...𝑁) ∖ ℙ) ∈ Fin
51 snfi 8079 . . . . . . 7 {2} ∈ Fin
52 unfi 8268 . . . . . . 7 ((((1...𝑁) ∖ ℙ) ∈ Fin ∧ {2} ∈ Fin) → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
5350, 51, 52mp2an 708 . . . . . 6 (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin
5453a1i 11 . . . . 5 (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
5512a1i 11 . . . . . 6 ((𝜑𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → Λ:ℕ⟶ℝ)
56 difss 3770 . . . . . . . . . 10 ((1...𝑁) ∖ ℙ) ⊆ (1...𝑁)
5756a1i 11 . . . . . . . . 9 (𝜑 → ((1...𝑁) ∖ ℙ) ⊆ (1...𝑁))
58 2nn 11223 . . . . . . . . . . . 12 2 ∈ ℕ
5958a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℕ)
60 hgt750lemb.2 . . . . . . . . . . 11 (𝜑 → 2 ≤ 𝑁)
61 elfz1b 12447 . . . . . . . . . . . 12 (2 ∈ (1...𝑁) ↔ (2 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 2 ≤ 𝑁))
6261biimpri 218 . . . . . . . . . . 11 ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 2 ≤ 𝑁) → 2 ∈ (1...𝑁))
6359, 1, 60, 62syl3anc 1366 . . . . . . . . . 10 (𝜑 → 2 ∈ (1...𝑁))
6463snssd 4372 . . . . . . . . 9 (𝜑 → {2} ⊆ (1...𝑁))
6557, 64unssd 3822 . . . . . . . 8 (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ (1...𝑁))
66 fz1ssnn 12410 . . . . . . . . 9 (1...𝑁) ⊆ ℕ
6766a1i 11 . . . . . . . 8 (𝜑 → (1...𝑁) ⊆ ℕ)
6865, 67sstrd 3646 . . . . . . 7 (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ ℕ)
6968sselda 3636 . . . . . 6 ((𝜑𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 𝑖 ∈ ℕ)
7055, 69ffvelrnd 6400 . . . . 5 ((𝜑𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (Λ‘𝑖) ∈ ℝ)
7154, 70fsumrecl 14509 . . . 4 (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) ∈ ℝ)
72 fzfid 12812 . . . . 5 (𝜑 → (1...𝑁) ∈ Fin)
7312a1i 11 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑁)) → Λ:ℕ⟶ℝ)
7467sselda 3636 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℕ)
7573, 74ffvelrnd 6400 . . . . 5 ((𝜑𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℝ)
7672, 75fsumrecl 14509 . . . 4 (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) ∈ ℝ)
7771, 76remulcld 10108 . . 3 (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ∈ ℝ)
7844, 77remulcld 10108 . 2 (𝜑 → ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ∈ ℝ)
791adantr 480 . . . . . . . 8 ((𝜑𝑛𝐴) → 𝑁 ∈ ℕ)
8079nnrpd 11908 . . . . . . 7 ((𝜑𝑛𝐴) → 𝑁 ∈ ℝ+)
81 relogcl 24367 . . . . . . 7 (𝑁 ∈ ℝ+ → (log‘𝑁) ∈ ℝ)
8280, 81syl 17 . . . . . 6 ((𝜑𝑛𝐴) → (log‘𝑁) ∈ ℝ)
8333, 82remulcld 10108 . . . . 5 ((𝜑𝑛𝐴) → ((Λ‘(𝑛‘1)) · (log‘𝑁)) ∈ ℝ)
8427, 83remulcld 10108 . . . 4 ((𝜑𝑛𝐴) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))) ∈ ℝ)
85 vmage0 24892 . . . . . 6 ((𝑛‘0) ∈ ℕ → 0 ≤ (Λ‘(𝑛‘0)))
8626, 85syl 17 . . . . 5 ((𝜑𝑛𝐴) → 0 ≤ (Λ‘(𝑛‘0)))
87 vmage0 24892 . . . . . . 7 ((𝑛‘1) ∈ ℕ → 0 ≤ (Λ‘(𝑛‘1)))
8832, 87syl 17 . . . . . 6 ((𝜑𝑛𝐴) → 0 ≤ (Λ‘(𝑛‘1)))
8938nnrpd 11908 . . . . . . . 8 ((𝜑𝑛𝐴) → (𝑛‘2) ∈ ℝ+)
9089relogcld 24414 . . . . . . 7 ((𝜑𝑛𝐴) → (log‘(𝑛‘2)) ∈ ℝ)
91 vmalelog 24975 . . . . . . . 8 ((𝑛‘2) ∈ ℕ → (Λ‘(𝑛‘2)) ≤ (log‘(𝑛‘2)))
9238, 91syl 17 . . . . . . 7 ((𝜑𝑛𝐴) → (Λ‘(𝑛‘2)) ≤ (log‘(𝑛‘2)))
9314, 16, 17, 19, 37reprle 30820 . . . . . . . 8 ((𝜑𝑛𝐴) → (𝑛‘2) ≤ 𝑁)
94 logleb 24394 . . . . . . . . 9 (((𝑛‘2) ∈ ℝ+𝑁 ∈ ℝ+) → ((𝑛‘2) ≤ 𝑁 ↔ (log‘(𝑛‘2)) ≤ (log‘𝑁)))
9594biimpa 500 . . . . . . . 8 ((((𝑛‘2) ∈ ℝ+𝑁 ∈ ℝ+) ∧ (𝑛‘2) ≤ 𝑁) → (log‘(𝑛‘2)) ≤ (log‘𝑁))
9689, 80, 93, 95syl21anc 1365 . . . . . . 7 ((𝜑𝑛𝐴) → (log‘(𝑛‘2)) ≤ (log‘𝑁))
9739, 90, 82, 92, 96letrd 10232 . . . . . 6 ((𝜑𝑛𝐴) → (Λ‘(𝑛‘2)) ≤ (log‘𝑁))
9839, 82, 33, 88, 97lemul2ad 11002 . . . . 5 ((𝜑𝑛𝐴) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ≤ ((Λ‘(𝑛‘1)) · (log‘𝑁)))
9940, 83, 27, 86, 98lemul2ad 11002 . . . 4 ((𝜑𝑛𝐴) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
10011, 41, 84, 99fsumle 14575 . . 3 (𝜑 → Σ𝑛𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ Σ𝑛𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
1011nncnd 11074 . . . . . 6 (𝜑𝑁 ∈ ℂ)
1021nnne0d 11103 . . . . . 6 (𝜑𝑁 ≠ 0)
103101, 102logcld 24362 . . . . 5 (𝜑 → (log‘𝑁) ∈ ℂ)
10445recnd 10106 . . . . 5 ((𝜑𝑛𝐴) → ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ∈ ℂ)
10511, 103, 104fsummulc2 14560 . . . 4 (𝜑 → ((log‘𝑁) · Σ𝑛𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) = Σ𝑛𝐴 ((log‘𝑁) · ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))))
106103adantr 480 . . . . . . 7 ((𝜑𝑛𝐴) → (log‘𝑁) ∈ ℂ)
107106, 104mulcomd 10099 . . . . . 6 ((𝜑𝑛𝐴) → ((log‘𝑁) · ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) = (((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) · (log‘𝑁)))
10827recnd 10106 . . . . . . 7 ((𝜑𝑛𝐴) → (Λ‘(𝑛‘0)) ∈ ℂ)
10933recnd 10106 . . . . . . 7 ((𝜑𝑛𝐴) → (Λ‘(𝑛‘1)) ∈ ℂ)
110108, 109, 106mulassd 10101 . . . . . 6 ((𝜑𝑛𝐴) → (((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) · (log‘𝑁)) = ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
111107, 110eqtrd 2685 . . . . 5 ((𝜑𝑛𝐴) → ((log‘𝑁) · ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) = ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
112111sumeq2dv 14477 . . . 4 (𝜑 → Σ𝑛𝐴 ((log‘𝑁) · ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) = Σ𝑛𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
113105, 112eqtr2d 2686 . . 3 (𝜑 → Σ𝑛𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))) = ((log‘𝑁) · Σ𝑛𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))))
114100, 113breqtrd 4711 . 2 (𝜑 → Σ𝑛𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · Σ𝑛𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))))
1151nnred 11073 . . . 4 (𝜑𝑁 ∈ ℝ)
1161nnge1d 11101 . . . 4 (𝜑 → 1 ≤ 𝑁)
117115, 116logge0d 24421 . . 3 (𝜑 → 0 ≤ (log‘𝑁))
118 xpfi 8272 . . . . . 6 (((((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) ∈ Fin)
11954, 72, 118syl2anc 694 . . . . 5 (𝜑 → ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) ∈ Fin)
12012a1i 11 . . . . . . 7 ((𝜑𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → Λ:ℕ⟶ℝ)
12168adantr 480 . . . . . . . 8 ((𝜑𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ ℕ)
122 xp1st 7242 . . . . . . . . 9 (𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) → (1st𝑢) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}))
123122adantl 481 . . . . . . . 8 ((𝜑𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (1st𝑢) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}))
124121, 123sseldd 3637 . . . . . . 7 ((𝜑𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (1st𝑢) ∈ ℕ)
125120, 124ffvelrnd 6400 . . . . . 6 ((𝜑𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (Λ‘(1st𝑢)) ∈ ℝ)
126 xp2nd 7243 . . . . . . . . 9 (𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) → (2nd𝑢) ∈ (1...𝑁))
127126adantl 481 . . . . . . . 8 ((𝜑𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (2nd𝑢) ∈ (1...𝑁))
12866, 127sseldi 3634 . . . . . . 7 ((𝜑𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (2nd𝑢) ∈ ℕ)
129120, 128ffvelrnd 6400 . . . . . 6 ((𝜑𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (Λ‘(2nd𝑢)) ∈ ℝ)
130125, 129remulcld 10108 . . . . 5 ((𝜑𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → ((Λ‘(1st𝑢)) · (Λ‘(2nd𝑢))) ∈ ℝ)
131 vmage0 24892 . . . . . . 7 ((1st𝑢) ∈ ℕ → 0 ≤ (Λ‘(1st𝑢)))
132124, 131syl 17 . . . . . 6 ((𝜑𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → 0 ≤ (Λ‘(1st𝑢)))
133 vmage0 24892 . . . . . . 7 ((2nd𝑢) ∈ ℕ → 0 ≤ (Λ‘(2nd𝑢)))
134128, 133syl 17 . . . . . 6 ((𝜑𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → 0 ≤ (Λ‘(2nd𝑢)))
135125, 129, 132, 134mulge0d 10642 . . . . 5 ((𝜑𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → 0 ≤ ((Λ‘(1st𝑢)) · (Λ‘(2nd𝑢))))
1365a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐴) → ℕ ⊆ ℕ)
13715adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐴) → 𝑁 ∈ ℤ)
1383a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐴) → 3 ∈ ℕ0)
139 simpr 476 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → 𝑐𝐴)
1409, 139sseldi 3634 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐴) → 𝑐 ∈ (ℕ(repr‘3)𝑁))
141136, 137, 138, 140reprf 30818 . . . . . . . . . . . . 13 ((𝜑𝑐𝐴) → 𝑐:(0..^3)⟶ℕ)
14224a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑐𝐴) → 0 ∈ (0..^3))
143141, 142ffvelrnd 6400 . . . . . . . . . . . 12 ((𝜑𝑐𝐴) → (𝑐‘0) ∈ ℕ)
1441adantr 480 . . . . . . . . . . . 12 ((𝜑𝑐𝐴) → 𝑁 ∈ ℕ)
145136, 137, 138, 140, 142reprle 30820 . . . . . . . . . . . 12 ((𝜑𝑐𝐴) → (𝑐‘0) ≤ 𝑁)
146 elfz1b 12447 . . . . . . . . . . . . 13 ((𝑐‘0) ∈ (1...𝑁) ↔ ((𝑐‘0) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘0) ≤ 𝑁))
147146biimpri 218 . . . . . . . . . . . 12 (((𝑐‘0) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘0) ≤ 𝑁) → (𝑐‘0) ∈ (1...𝑁))
148143, 144, 145, 147syl3anc 1366 . . . . . . . . . . 11 ((𝜑𝑐𝐴) → (𝑐‘0) ∈ (1...𝑁))
1498rabeq2i 3228 . . . . . . . . . . . . . 14 (𝑐𝐴 ↔ (𝑐 ∈ (ℕ(repr‘3)𝑁) ∧ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)))
150149simprbi 479 . . . . . . . . . . . . 13 (𝑐𝐴 → ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ))
151 hgt750leme.o . . . . . . . . . . . . . . 15 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
152151oddprm2 30861 . . . . . . . . . . . . . 14 (ℙ ∖ {2}) = (𝑂 ∩ ℙ)
153152eleq2i 2722 . . . . . . . . . . . . 13 ((𝑐‘0) ∈ (ℙ ∖ {2}) ↔ (𝑐‘0) ∈ (𝑂 ∩ ℙ))
154150, 153sylnibr 318 . . . . . . . . . . . 12 (𝑐𝐴 → ¬ (𝑐‘0) ∈ (ℙ ∖ {2}))
155139, 154syl 17 . . . . . . . . . . 11 ((𝜑𝑐𝐴) → ¬ (𝑐‘0) ∈ (ℙ ∖ {2}))
156148, 155jca 553 . . . . . . . . . 10 ((𝜑𝑐𝐴) → ((𝑐‘0) ∈ (1...𝑁) ∧ ¬ (𝑐‘0) ∈ (ℙ ∖ {2})))
157 eldif 3617 . . . . . . . . . 10 ((𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖ {2})) ↔ ((𝑐‘0) ∈ (1...𝑁) ∧ ¬ (𝑐‘0) ∈ (ℙ ∖ {2})))
158156, 157sylibr 224 . . . . . . . . 9 ((𝜑𝑐𝐴) → (𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖ {2})))
159 uncom 3790 . . . . . . . . . . . . 13 (((1...𝑁) ∖ ℙ) ∪ {2}) = ({2} ∪ ((1...𝑁) ∖ ℙ))
160 undif3 3921 . . . . . . . . . . . . 13 ({2} ∪ ((1...𝑁) ∖ ℙ)) = (({2} ∪ (1...𝑁)) ∖ (ℙ ∖ {2}))
161159, 160eqtri 2673 . . . . . . . . . . . 12 (((1...𝑁) ∖ ℙ) ∪ {2}) = (({2} ∪ (1...𝑁)) ∖ (ℙ ∖ {2}))
162 ssequn1 3816 . . . . . . . . . . . . . 14 ({2} ⊆ (1...𝑁) ↔ ({2} ∪ (1...𝑁)) = (1...𝑁))
16364, 162sylib 208 . . . . . . . . . . . . 13 (𝜑 → ({2} ∪ (1...𝑁)) = (1...𝑁))
164163difeq1d 3760 . . . . . . . . . . . 12 (𝜑 → (({2} ∪ (1...𝑁)) ∖ (ℙ ∖ {2})) = ((1...𝑁) ∖ (ℙ ∖ {2})))
165161, 164syl5eq 2697 . . . . . . . . . . 11 (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) = ((1...𝑁) ∖ (ℙ ∖ {2})))
166165eleq2d 2716 . . . . . . . . . 10 (𝜑 → ((𝑐‘0) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ↔ (𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖ {2}))))
167166adantr 480 . . . . . . . . 9 ((𝜑𝑐𝐴) → ((𝑐‘0) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ↔ (𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖ {2}))))
168158, 167mpbird 247 . . . . . . . 8 ((𝜑𝑐𝐴) → (𝑐‘0) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}))
16930a1i 11 . . . . . . . . . 10 ((𝜑𝑐𝐴) → 1 ∈ (0..^3))
170141, 169ffvelrnd 6400 . . . . . . . . 9 ((𝜑𝑐𝐴) → (𝑐‘1) ∈ ℕ)
171136, 137, 138, 140, 169reprle 30820 . . . . . . . . 9 ((𝜑𝑐𝐴) → (𝑐‘1) ≤ 𝑁)
172 elfz1b 12447 . . . . . . . . . 10 ((𝑐‘1) ∈ (1...𝑁) ↔ ((𝑐‘1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘1) ≤ 𝑁))
173172biimpri 218 . . . . . . . . 9 (((𝑐‘1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘1) ≤ 𝑁) → (𝑐‘1) ∈ (1...𝑁))
174170, 144, 171, 173syl3anc 1366 . . . . . . . 8 ((𝜑𝑐𝐴) → (𝑐‘1) ∈ (1...𝑁))
175168, 174opelxpd 5183 . . . . . . 7 ((𝜑𝑐𝐴) → ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
176175ralrimiva 2995 . . . . . 6 (𝜑 → ∀𝑐𝐴 ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
177 fveq1 6228 . . . . . . . . 9 (𝑑 = 𝑐 → (𝑑‘0) = (𝑐‘0))
178 fveq1 6228 . . . . . . . . 9 (𝑑 = 𝑐 → (𝑑‘1) = (𝑐‘1))
179177, 178opeq12d 4441 . . . . . . . 8 (𝑑 = 𝑐 → ⟨(𝑑‘0), (𝑑‘1)⟩ = ⟨(𝑐‘0), (𝑐‘1)⟩)
180179cbvmptv 4783 . . . . . . 7 (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = (𝑐𝐴 ↦ ⟨(𝑐‘0), (𝑐‘1)⟩)
181180rnmptss 6432 . . . . . 6 (∀𝑐𝐴 ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) → ran (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) ⊆ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
182176, 181syl 17 . . . . 5 (𝜑 → ran (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) ⊆ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
183119, 130, 135, 182fsumless 14572 . . . 4 (𝜑 → Σ𝑢 ∈ ran (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)((Λ‘(1st𝑢)) · (Λ‘(2nd𝑢))) ≤ Σ𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))((Λ‘(1st𝑢)) · (Λ‘(2nd𝑢))))
184 fvex 6239 . . . . . . . 8 (𝑛‘0) ∈ V
185 fvex 6239 . . . . . . . 8 (𝑛‘1) ∈ V
186184, 185op1std 7220 . . . . . . 7 (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → (1st𝑢) = (𝑛‘0))
187186fveq2d 6233 . . . . . 6 (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → (Λ‘(1st𝑢)) = (Λ‘(𝑛‘0)))
188184, 185op2ndd 7221 . . . . . . 7 (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → (2nd𝑢) = (𝑛‘1))
189188fveq2d 6233 . . . . . 6 (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → (Λ‘(2nd𝑢)) = (Λ‘(𝑛‘1)))
190187, 189oveq12d 6708 . . . . 5 (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → ((Λ‘(1st𝑢)) · (Λ‘(2nd𝑢))) = ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))))
191 opex 4962 . . . . . . . 8 ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ V
192191rgenw 2953 . . . . . . 7 𝑐𝐴 ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ V
193180fnmpt 6058 . . . . . . 7 (∀𝑐𝐴 ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ V → (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) Fn 𝐴)
194192, 193mp1i 13 . . . . . 6 (𝜑 → (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) Fn 𝐴)
195 eqidd 2652 . . . . . 6 (𝜑 → ran (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = ran (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩))
196141ad2antrr 762 . . . . . . . . . . 11 ((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑐:(0..^3)⟶ℕ)
197196ffnd 6084 . . . . . . . . . 10 ((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑐 Fn (0..^3))
19820ad4ant13 1315 . . . . . . . . . . 11 ((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑛:(0..^3)⟶ℕ)
199198ffnd 6084 . . . . . . . . . 10 ((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑛 Fn (0..^3))
200 simpr 476 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛))
201180a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = (𝑐𝐴 ↦ ⟨(𝑐‘0), (𝑐‘1)⟩))
202191a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴) → ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ V)
203201, 202fvmpt2d 6332 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴) → ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ⟨(𝑐‘0), (𝑐‘1)⟩)
204203adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐴) ∧ 𝑛𝐴) → ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ⟨(𝑐‘0), (𝑐‘1)⟩)
205204adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ⟨(𝑐‘0), (𝑐‘1)⟩)
206180a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛𝐴) → (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = (𝑐𝐴 ↦ ⟨(𝑐‘0), (𝑐‘1)⟩))
207 fveq1 6228 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = 𝑛 → (𝑐‘0) = (𝑛‘0))
208 fveq1 6228 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = 𝑛 → (𝑐‘1) = (𝑛‘1))
209207, 208opeq12d 4441 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑛 → ⟨(𝑐‘0), (𝑐‘1)⟩ = ⟨(𝑛‘0), (𝑛‘1)⟩)
210209adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛𝐴) ∧ 𝑐 = 𝑛) → ⟨(𝑐‘0), (𝑐‘1)⟩ = ⟨(𝑛‘0), (𝑛‘1)⟩)
211 opex 4962 . . . . . . . . . . . . . . . . . . . 20 ⟨(𝑛‘0), (𝑛‘1)⟩ ∈ V
212211a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛𝐴) → ⟨(𝑛‘0), (𝑛‘1)⟩ ∈ V)
213206, 210, 18, 212fvmptd 6327 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐴) → ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) = ⟨(𝑛‘0), (𝑛‘1)⟩)
214213adantlr 751 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐴) ∧ 𝑛𝐴) → ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) = ⟨(𝑛‘0), (𝑛‘1)⟩)
215214adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) = ⟨(𝑛‘0), (𝑛‘1)⟩)
216200, 205, 2153eqtr3d 2693 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ⟨(𝑐‘0), (𝑐‘1)⟩ = ⟨(𝑛‘0), (𝑛‘1)⟩)
217184, 185opth2 4978 . . . . . . . . . . . . . . 15 (⟨(𝑐‘0), (𝑐‘1)⟩ = ⟨(𝑛‘0), (𝑛‘1)⟩ ↔ ((𝑐‘0) = (𝑛‘0) ∧ (𝑐‘1) = (𝑛‘1)))
218216, 217sylib 208 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ((𝑐‘0) = (𝑛‘0) ∧ (𝑐‘1) = (𝑛‘1)))
219218simpld 474 . . . . . . . . . . . . 13 ((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → (𝑐‘0) = (𝑛‘0))
220219ad2antrr 762 . . . . . . . . . . . 12 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑐‘0) = (𝑛‘0))
221 simpr 476 . . . . . . . . . . . . 13 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → 𝑖 = 0)
222221fveq2d 6233 . . . . . . . . . . . 12 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑐𝑖) = (𝑐‘0))
223221fveq2d 6233 . . . . . . . . . . . 12 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑛𝑖) = (𝑛‘0))
224220, 222, 2233eqtr4d 2695 . . . . . . . . . . 11 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑐𝑖) = (𝑛𝑖))
225218simprd 478 . . . . . . . . . . . . 13 ((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → (𝑐‘1) = (𝑛‘1))
226225ad2antrr 762 . . . . . . . . . . . 12 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑐‘1) = (𝑛‘1))
227 simpr 476 . . . . . . . . . . . . 13 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → 𝑖 = 1)
228227fveq2d 6233 . . . . . . . . . . . 12 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑐𝑖) = (𝑐‘1))
229227fveq2d 6233 . . . . . . . . . . . 12 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑛𝑖) = (𝑛‘1))
230226, 228, 2293eqtr4d 2695 . . . . . . . . . . 11 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑐𝑖) = (𝑛𝑖))
231219ad2antrr 762 . . . . . . . . . . . . . . 15 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘0) = (𝑛‘0))
232225ad2antrr 762 . . . . . . . . . . . . . . 15 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘1) = (𝑛‘1))
233231, 232oveq12d 6708 . . . . . . . . . . . . . 14 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑐‘0) + (𝑐‘1)) = ((𝑛‘0) + (𝑛‘1)))
234233oveq2d 6706 . . . . . . . . . . . . 13 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑁 − ((𝑐‘0) + (𝑐‘1))) = (𝑁 − ((𝑛‘0) + (𝑛‘1))))
23523a1i 11 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (0..^3) = {0, 1, 2})
236235sumeq1d 14475 . . . . . . . . . . . . . . 15 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑐𝑗) = Σ𝑗 ∈ {0, 1, 2} (𝑐𝑗))
2375a1i 11 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ℕ ⊆ ℕ)
238137ad4antr 769 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑁 ∈ ℤ)
2393a1i 11 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 3 ∈ ℕ0)
240140ad4antr 769 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑐 ∈ (ℕ(repr‘3)𝑁))
241237, 238, 239, 240reprsum 30819 . . . . . . . . . . . . . . 15 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑐𝑗) = 𝑁)
242 fveq2 6229 . . . . . . . . . . . . . . . 16 (𝑗 = 0 → (𝑐𝑗) = (𝑐‘0))
243 fveq2 6229 . . . . . . . . . . . . . . . 16 (𝑗 = 1 → (𝑐𝑗) = (𝑐‘1))
244 fveq2 6229 . . . . . . . . . . . . . . . 16 (𝑗 = 2 → (𝑐𝑗) = (𝑐‘2))
245143nncnd 11074 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴) → (𝑐‘0) ∈ ℂ)
246245ad4antr 769 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘0) ∈ ℂ)
247170nncnd 11074 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴) → (𝑐‘1) ∈ ℂ)
248247ad4antr 769 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘1) ∈ ℂ)
24936a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐴) → 2 ∈ (0..^3))
250141, 249ffvelrnd 6400 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴) → (𝑐‘2) ∈ ℕ)
251250nncnd 11074 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴) → (𝑐‘2) ∈ ℂ)
252251ad4antr 769 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘2) ∈ ℂ)
253246, 248, 2523jca 1261 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑐‘0) ∈ ℂ ∧ (𝑐‘1) ∈ ℂ ∧ (𝑐‘2) ∈ ℂ))
25421, 28, 343pm3.2i 1259 . . . . . . . . . . . . . . . . 17 (0 ∈ V ∧ 1 ∈ V ∧ 2 ∈ V)
255254a1i 11 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (0 ∈ V ∧ 1 ∈ V ∧ 2 ∈ V))
256 0ne1 11126 . . . . . . . . . . . . . . . . 17 0 ≠ 1
257256a1i 11 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 0 ≠ 1)
258 0ne2 11277 . . . . . . . . . . . . . . . . 17 0 ≠ 2
259258a1i 11 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 0 ≠ 2)
260 1ne2 11278 . . . . . . . . . . . . . . . . 17 1 ≠ 2
261260a1i 11 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 1 ≠ 2)
262242, 243, 244, 253, 255, 257, 259, 261sumtp 14522 . . . . . . . . . . . . . . 15 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ {0, 1, 2} (𝑐𝑗) = (((𝑐‘0) + (𝑐‘1)) + (𝑐‘2)))
263236, 241, 2623eqtr3rd 2694 . . . . . . . . . . . . . 14 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (((𝑐‘0) + (𝑐‘1)) + (𝑐‘2)) = 𝑁)
264246, 248addcld 10097 . . . . . . . . . . . . . . 15 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑐‘0) + (𝑐‘1)) ∈ ℂ)
265101ad5antr 773 . . . . . . . . . . . . . . 15 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑁 ∈ ℂ)
266264, 252, 265addrsub 10486 . . . . . . . . . . . . . 14 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((((𝑐‘0) + (𝑐‘1)) + (𝑐‘2)) = 𝑁 ↔ (𝑐‘2) = (𝑁 − ((𝑐‘0) + (𝑐‘1)))))
267263, 266mpbid 222 . . . . . . . . . . . . 13 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘2) = (𝑁 − ((𝑐‘0) + (𝑐‘1))))
268235sumeq1d 14475 . . . . . . . . . . . . . . 15 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑛𝑗) = Σ𝑗 ∈ {0, 1, 2} (𝑛𝑗))
26919ad4ant13 1315 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
270269ad2antrr 762 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
271237, 238, 239, 270reprsum 30819 . . . . . . . . . . . . . . 15 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑛𝑗) = 𝑁)
272 fveq2 6229 . . . . . . . . . . . . . . . 16 (𝑗 = 0 → (𝑛𝑗) = (𝑛‘0))
273 fveq2 6229 . . . . . . . . . . . . . . . 16 (𝑗 = 1 → (𝑛𝑗) = (𝑛‘1))
274 fveq2 6229 . . . . . . . . . . . . . . . 16 (𝑗 = 2 → (𝑛𝑗) = (𝑛‘2))
27526nncnd 11074 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛𝐴) → (𝑛‘0) ∈ ℂ)
276275adantlr 751 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐴) ∧ 𝑛𝐴) → (𝑛‘0) ∈ ℂ)
277276ad3antrrr 766 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘0) ∈ ℂ)
27832nncnd 11074 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛𝐴) → (𝑛‘1) ∈ ℂ)
279278adantlr 751 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐴) ∧ 𝑛𝐴) → (𝑛‘1) ∈ ℂ)
280279ad3antrrr 766 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘1) ∈ ℂ)
28138nncnd 11074 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛𝐴) → (𝑛‘2) ∈ ℂ)
282281adantlr 751 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐴) ∧ 𝑛𝐴) → (𝑛‘2) ∈ ℂ)
283282ad3antrrr 766 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘2) ∈ ℂ)
284277, 280, 2833jca 1261 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑛‘0) ∈ ℂ ∧ (𝑛‘1) ∈ ℂ ∧ (𝑛‘2) ∈ ℂ))
285272, 273, 274, 284, 255, 257, 259, 261sumtp 14522 . . . . . . . . . . . . . . 15 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ {0, 1, 2} (𝑛𝑗) = (((𝑛‘0) + (𝑛‘1)) + (𝑛‘2)))
286268, 271, 2853eqtr3rd 2694 . . . . . . . . . . . . . 14 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (((𝑛‘0) + (𝑛‘1)) + (𝑛‘2)) = 𝑁)
287277, 280addcld 10097 . . . . . . . . . . . . . . 15 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑛‘0) + (𝑛‘1)) ∈ ℂ)
288287, 283, 265addrsub 10486 . . . . . . . . . . . . . 14 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((((𝑛‘0) + (𝑛‘1)) + (𝑛‘2)) = 𝑁 ↔ (𝑛‘2) = (𝑁 − ((𝑛‘0) + (𝑛‘1)))))
289286, 288mpbid 222 . . . . . . . . . . . . 13 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘2) = (𝑁 − ((𝑛‘0) + (𝑛‘1))))
290234, 267, 2893eqtr4d 2695 . . . . . . . . . . . 12 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘2) = (𝑛‘2))
291 simpr 476 . . . . . . . . . . . . 13 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑖 = 2)
292291fveq2d 6233 . . . . . . . . . . . 12 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐𝑖) = (𝑐‘2))
293291fveq2d 6233 . . . . . . . . . . . 12 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛𝑖) = (𝑛‘2))
294290, 292, 2933eqtr4d 2695 . . . . . . . . . . 11 ((((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐𝑖) = (𝑛𝑖))
295 simpr 476 . . . . . . . . . . . . 13 (((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → 𝑖 ∈ (0..^3))
296295, 23syl6eleq 2740 . . . . . . . . . . . 12 (((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → 𝑖 ∈ {0, 1, 2})
297 vex 3234 . . . . . . . . . . . . 13 𝑖 ∈ V
298297eltp 4262 . . . . . . . . . . . 12 (𝑖 ∈ {0, 1, 2} ↔ (𝑖 = 0 ∨ 𝑖 = 1 ∨ 𝑖 = 2))
299296, 298sylib 208 . . . . . . . . . . 11 (((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → (𝑖 = 0 ∨ 𝑖 = 1 ∨ 𝑖 = 2))
300224, 230, 294, 299mpjao3dan 1435 . . . . . . . . . 10 (((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → (𝑐𝑖) = (𝑛𝑖))
301197, 199, 300eqfnfvd 6354 . . . . . . . . 9 ((((𝜑𝑐𝐴) ∧ 𝑛𝐴) ∧ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑐 = 𝑛)
302301ex 449 . . . . . . . 8 (((𝜑𝑐𝐴) ∧ 𝑛𝐴) → (((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛))
303302anasss 680 . . . . . . 7 ((𝜑 ∧ (𝑐𝐴𝑛𝐴)) → (((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛))
304303ralrimivva 3000 . . . . . 6 (𝜑 → ∀𝑐𝐴𝑛𝐴 (((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛))
305 dff1o6 6571 . . . . . . 7 ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩):𝐴1-1-onto→ran (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) ↔ ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) Fn 𝐴 ∧ ran (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = ran (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) ∧ ∀𝑐𝐴𝑛𝐴 (((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛)))
306305biimpri 218 . . . . . 6 (((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) Fn 𝐴 ∧ ran (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = ran (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) ∧ ∀𝑐𝐴𝑛𝐴 (((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛)) → (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩):𝐴1-1-onto→ran (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩))
307194, 195, 304, 306syl3anc 1366 . . . . 5 (𝜑 → (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩):𝐴1-1-onto→ran (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩))
308182sselda 3636 . . . . . . . 8 ((𝜑𝑢 ∈ ran (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
309308, 125syldan 486 . . . . . . 7 ((𝜑𝑢 ∈ ran (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → (Λ‘(1st𝑢)) ∈ ℝ)
310308, 129syldan 486 . . . . . . 7 ((𝜑𝑢 ∈ ran (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → (Λ‘(2nd𝑢)) ∈ ℝ)
311309, 310remulcld 10108 . . . . . 6 ((𝜑𝑢 ∈ ran (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → ((Λ‘(1st𝑢)) · (Λ‘(2nd𝑢))) ∈ ℝ)
312311recnd 10106 . . . . 5 ((𝜑𝑢 ∈ ran (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → ((Λ‘(1st𝑢)) · (Λ‘(2nd𝑢))) ∈ ℂ)
313190, 11, 307, 213, 312fsumf1o 14498 . . . 4 (𝜑 → Σ𝑢 ∈ ran (𝑑𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)((Λ‘(1st𝑢)) · (Λ‘(2nd𝑢))) = Σ𝑛𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))))
31476recnd 10106 . . . . . 6 (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) ∈ ℂ)
31570recnd 10106 . . . . . 6 ((𝜑𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (Λ‘𝑖) ∈ ℂ)
31654, 314, 315fsummulc1 14561 . . . . 5 (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) = Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})((Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))
31748a1i 11 . . . . . . 7 ((𝜑𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (1...𝑁) ∈ Fin)
31875adantrl 752 . . . . . . . . 9 ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → (Λ‘𝑗) ∈ ℝ)
319318anassrs 681 . . . . . . . 8 (((𝜑𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℝ)
320319recnd 10106 . . . . . . 7 (((𝜑𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℂ)
321317, 315, 320fsummulc2 14560 . . . . . 6 ((𝜑𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → ((Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) = Σ𝑗 ∈ (1...𝑁)((Λ‘𝑖) · (Λ‘𝑗)))
322321sumeq2dv 14477 . . . . 5 (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})((Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) = Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})Σ𝑗 ∈ (1...𝑁)((Λ‘𝑖) · (Λ‘𝑗)))
323 vex 3234 . . . . . . . . 9 𝑗 ∈ V
324297, 323op1std 7220 . . . . . . . 8 (𝑢 = ⟨𝑖, 𝑗⟩ → (1st𝑢) = 𝑖)
325324fveq2d 6233 . . . . . . 7 (𝑢 = ⟨𝑖, 𝑗⟩ → (Λ‘(1st𝑢)) = (Λ‘𝑖))
326297, 323op2ndd 7221 . . . . . . . 8 (𝑢 = ⟨𝑖, 𝑗⟩ → (2nd𝑢) = 𝑗)
327326fveq2d 6233 . . . . . . 7 (𝑢 = ⟨𝑖, 𝑗⟩ → (Λ‘(2nd𝑢)) = (Λ‘𝑗))
328325, 327oveq12d 6708 . . . . . 6 (𝑢 = ⟨𝑖, 𝑗⟩ → ((Λ‘(1st𝑢)) · (Λ‘(2nd𝑢))) = ((Λ‘𝑖) · (Λ‘𝑗)))
32970adantrr 753 . . . . . . . 8 ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → (Λ‘𝑖) ∈ ℝ)
330329, 318remulcld 10108 . . . . . . 7 ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → ((Λ‘𝑖) · (Λ‘𝑗)) ∈ ℝ)
331330recnd 10106 . . . . . 6 ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → ((Λ‘𝑖) · (Λ‘𝑗)) ∈ ℂ)
332328, 54, 72, 331fsumxp 14547 . . . . 5 (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})Σ𝑗 ∈ (1...𝑁)((Λ‘𝑖) · (Λ‘𝑗)) = Σ𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))((Λ‘(1st𝑢)) · (Λ‘(2nd𝑢))))
333316, 322, 3323eqtrrd 2690 . . . 4 (𝜑 → Σ𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))((Λ‘(1st𝑢)) · (Λ‘(2nd𝑢))) = (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))
334183, 313, 3333brtr3d 4716 . . 3 (𝜑 → Σ𝑛𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ≤ (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))
33546, 77, 44, 117, 334lemul2ad 11002 . 2 (𝜑 → ((log‘𝑁) · Σ𝑛𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))
33642, 47, 78, 114, 335letrd 10232 1 (𝜑 → Σ𝑛𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∨ w3o 1053   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  {crab 2945  Vcvv 3231   ∖ cdif 3604   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  {csn 4210  {ctp 4214  ⟨cop 4216   class class class wbr 4685   ↦ cmpt 4762   × cxp 5141  ran crn 5144   Fn wfn 5921  ⟶wf 5922  –1-1-onto→wf1o 5925  ‘cfv 5926  (class class class)co 6690  1st c1st 7208  2nd c2nd 7209  Fincfn 7997  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   ≤ cle 10113   − cmin 10304  ℕcn 11058  2c2 11108  3c3 11109  ℕ0cn0 11330  ℤcz 11415  ℝ+crp 11870  ...cfz 12364  ..^cfzo 12504  Σcsu 14460   ∥ cdvds 15027  ℙcprime 15432  logclog 24346  Λcvma 24863  reprcrepr 30814 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ioc 12218  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-fac 13101  df-bc 13130  df-hash 13158  df-shft 13851  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-sum 14461  df-ef 14842  df-sin 14844  df-cos 14845  df-pi 14847  df-dvds 15028  df-gcd 15264  df-prm 15433  df-pc 15589  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-mulg 17588  df-cntz 17796  df-cmn 18241  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-fbas 19791  df-fg 19792  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-lp 20988  df-perf 20989  df-cn 21079  df-cnp 21080  df-haus 21167  df-tx 21413  df-hmeo 21606  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-xms 22172  df-ms 22173  df-tms 22174  df-cncf 22728  df-limc 23675  df-dv 23676  df-log 24348  df-vma 24869  df-repr 30815 This theorem is referenced by:  hgt750leme  30864
 Copyright terms: Public domain W3C validator