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

Theorem hgt750leme 33969
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, 29-Dec-2021.)
Hypotheses
Ref Expression
hgt750leme.o 𝑂 = {𝑧 ∈ β„€ ∣ Β¬ 2 βˆ₯ 𝑧}
hgt750leme.n (πœ‘ β†’ 𝑁 ∈ β„•)
hgt750leme.0 (πœ‘ β†’ (10↑27) ≀ 𝑁)
hgt750leme.h (πœ‘ β†’ 𝐻:β„•βŸΆ(0[,)+∞))
hgt750leme.k (πœ‘ β†’ 𝐾:β„•βŸΆ(0[,)+∞))
hgt750leme.1 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (πΎβ€˜π‘š) ≀ (1.079955))
hgt750leme.2 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (π»β€˜π‘š) ≀ (1.414))
Assertion
Ref Expression
hgt750leme (πœ‘ β†’ Σ𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))(((Ξ›β€˜(π‘›β€˜0)) Β· (π»β€˜(π‘›β€˜0))) Β· (((Ξ›β€˜(π‘›β€˜1)) Β· (πΎβ€˜(π‘›β€˜1))) Β· ((Ξ›β€˜(π‘›β€˜2)) Β· (πΎβ€˜(π‘›β€˜2))))) ≀ (((7.348) Β· ((logβ€˜π‘) / (βˆšβ€˜π‘))) Β· (𝑁↑2)))
Distinct variable groups:   𝑧,𝑂   π‘š,𝐻   π‘š,𝐾   π‘š,𝑁,𝑛   π‘š,𝑂,𝑛,𝑧   πœ‘,π‘š,𝑛
Allowed substitution hints:   πœ‘(𝑧)   𝐻(𝑧,𝑛)   𝐾(𝑧,𝑛)   𝑁(𝑧)

Proof of Theorem hgt750leme
Dummy variables π‘Ž 𝑐 𝑑 𝑒 𝑖 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hgt750leme.n . . . . . 6 (πœ‘ β†’ 𝑁 ∈ β„•)
21nnnn0d 12537 . . . . 5 (πœ‘ β†’ 𝑁 ∈ β„•0)
3 3nn0 12495 . . . . . 6 3 ∈ β„•0
43a1i 11 . . . . 5 (πœ‘ β†’ 3 ∈ β„•0)
5 ssidd 4005 . . . . 5 (πœ‘ β†’ β„• βŠ† β„•)
62, 4, 5reprfi2 33934 . . . 4 (πœ‘ β†’ (β„•(reprβ€˜3)𝑁) ∈ Fin)
7 diffi 9183 . . . 4 ((β„•(reprβ€˜3)𝑁) ∈ Fin β†’ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁)) ∈ Fin)
86, 7syl 17 . . 3 (πœ‘ β†’ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁)) ∈ Fin)
9 vmaf 26860 . . . . . . 7 Ξ›:β„•βŸΆβ„
109a1i 11 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ Ξ›:β„•βŸΆβ„)
11 ssidd 4005 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ β„• βŠ† β„•)
121nnzd 12590 . . . . . . . . 9 (πœ‘ β†’ 𝑁 ∈ β„€)
1312adantr 480 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 𝑁 ∈ β„€)
143a1i 11 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 3 ∈ β„•0)
15 simpr 484 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁)))
1615eldifad 3960 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 𝑛 ∈ (β„•(reprβ€˜3)𝑁))
1711, 13, 14, 16reprf 33923 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 𝑛:(0..^3)βŸΆβ„•)
18 c0ex 11213 . . . . . . . . . 10 0 ∈ V
1918tpid1 4772 . . . . . . . . 9 0 ∈ {0, 1, 2}
20 fzo0to3tp 13723 . . . . . . . . 9 (0..^3) = {0, 1, 2}
2119, 20eleqtrri 2831 . . . . . . . 8 0 ∈ (0..^3)
2221a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 0 ∈ (0..^3))
2317, 22ffvelcdmd 7087 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (π‘›β€˜0) ∈ β„•)
2410, 23ffvelcdmd 7087 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (Ξ›β€˜(π‘›β€˜0)) ∈ ℝ)
25 rge0ssre 13438 . . . . . 6 (0[,)+∞) βŠ† ℝ
26 hgt750leme.h . . . . . . . 8 (πœ‘ β†’ 𝐻:β„•βŸΆ(0[,)+∞))
2726adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 𝐻:β„•βŸΆ(0[,)+∞))
2827, 23ffvelcdmd 7087 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (π»β€˜(π‘›β€˜0)) ∈ (0[,)+∞))
2925, 28sselid 3980 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (π»β€˜(π‘›β€˜0)) ∈ ℝ)
3024, 29remulcld 11249 . . . 4 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ ((Ξ›β€˜(π‘›β€˜0)) Β· (π»β€˜(π‘›β€˜0))) ∈ ℝ)
31 1ex 11215 . . . . . . . . . . 11 1 ∈ V
3231tpid2 4774 . . . . . . . . . 10 1 ∈ {0, 1, 2}
3332, 20eleqtrri 2831 . . . . . . . . 9 1 ∈ (0..^3)
3433a1i 11 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 1 ∈ (0..^3))
3517, 34ffvelcdmd 7087 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (π‘›β€˜1) ∈ β„•)
3610, 35ffvelcdmd 7087 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (Ξ›β€˜(π‘›β€˜1)) ∈ ℝ)
37 hgt750leme.k . . . . . . . . 9 (πœ‘ β†’ 𝐾:β„•βŸΆ(0[,)+∞))
3837adantr 480 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 𝐾:β„•βŸΆ(0[,)+∞))
3938, 35ffvelcdmd 7087 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (πΎβ€˜(π‘›β€˜1)) ∈ (0[,)+∞))
4025, 39sselid 3980 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (πΎβ€˜(π‘›β€˜1)) ∈ ℝ)
4136, 40remulcld 11249 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ ((Ξ›β€˜(π‘›β€˜1)) Β· (πΎβ€˜(π‘›β€˜1))) ∈ ℝ)
42 2ex 12294 . . . . . . . . . . 11 2 ∈ V
4342tpid3 4777 . . . . . . . . . 10 2 ∈ {0, 1, 2}
4443, 20eleqtrri 2831 . . . . . . . . 9 2 ∈ (0..^3)
4544a1i 11 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 2 ∈ (0..^3))
4617, 45ffvelcdmd 7087 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (π‘›β€˜2) ∈ β„•)
4710, 46ffvelcdmd 7087 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (Ξ›β€˜(π‘›β€˜2)) ∈ ℝ)
4838, 46ffvelcdmd 7087 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (πΎβ€˜(π‘›β€˜2)) ∈ (0[,)+∞))
4925, 48sselid 3980 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (πΎβ€˜(π‘›β€˜2)) ∈ ℝ)
5047, 49remulcld 11249 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ ((Ξ›β€˜(π‘›β€˜2)) Β· (πΎβ€˜(π‘›β€˜2))) ∈ ℝ)
5141, 50remulcld 11249 . . . 4 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (((Ξ›β€˜(π‘›β€˜1)) Β· (πΎβ€˜(π‘›β€˜1))) Β· ((Ξ›β€˜(π‘›β€˜2)) Β· (πΎβ€˜(π‘›β€˜2)))) ∈ ℝ)
5230, 51remulcld 11249 . . 3 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (((Ξ›β€˜(π‘›β€˜0)) Β· (π»β€˜(π‘›β€˜0))) Β· (((Ξ›β€˜(π‘›β€˜1)) Β· (πΎβ€˜(π‘›β€˜1))) Β· ((Ξ›β€˜(π‘›β€˜2)) Β· (πΎβ€˜(π‘›β€˜2))))) ∈ ℝ)
538, 52fsumrecl 15685 . 2 (πœ‘ β†’ Σ𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))(((Ξ›β€˜(π‘›β€˜0)) Β· (π»β€˜(π‘›β€˜0))) Β· (((Ξ›β€˜(π‘›β€˜1)) Β· (πΎβ€˜(π‘›β€˜1))) Β· ((Ξ›β€˜(π‘›β€˜2)) Β· (πΎβ€˜(π‘›β€˜2))))) ∈ ℝ)
54 3re 12297 . . . 4 3 ∈ ℝ
5554a1i 11 . . 3 (πœ‘ β†’ 3 ∈ ℝ)
56 1nn0 12493 . . . . . . . . 9 1 ∈ β„•0
57 0nn0 12492 . . . . . . . . . 10 0 ∈ β„•0
58 7nn0 12499 . . . . . . . . . . 11 7 ∈ β„•0
59 9nn0 12501 . . . . . . . . . . . 12 9 ∈ β„•0
60 5nn0 12497 . . . . . . . . . . . . . 14 5 ∈ β„•0
61 5nn 12303 . . . . . . . . . . . . . . 15 5 ∈ β„•
62 nnrp 12990 . . . . . . . . . . . . . . 15 (5 ∈ β„• β†’ 5 ∈ ℝ+)
6361, 62ax-mp 5 . . . . . . . . . . . . . 14 5 ∈ ℝ+
6460, 63rpdp2cl 32316 . . . . . . . . . . . . 13 55 ∈ ℝ+
6559, 64rpdp2cl 32316 . . . . . . . . . . . 12 955 ∈ ℝ+
6659, 65rpdp2cl 32316 . . . . . . . . . . 11 9955 ∈ ℝ+
6758, 66rpdp2cl 32316 . . . . . . . . . 10 79955 ∈ ℝ+
6857, 67rpdp2cl 32316 . . . . . . . . 9 079955 ∈ ℝ+
6956, 68rpdpcl 32337 . . . . . . . 8 (1.079955) ∈ ℝ+
7069a1i 11 . . . . . . 7 (πœ‘ β†’ (1.079955) ∈ ℝ+)
7170rpred 13021 . . . . . 6 (πœ‘ β†’ (1.079955) ∈ ℝ)
7271resqcld 14095 . . . . 5 (πœ‘ β†’ ((1.079955)↑2) ∈ ℝ)
73 4nn0 12496 . . . . . . . . 9 4 ∈ β„•0
74 4nn 12300 . . . . . . . . . . 11 4 ∈ β„•
75 nnrp 12990 . . . . . . . . . . 11 (4 ∈ β„• β†’ 4 ∈ ℝ+)
7674, 75ax-mp 5 . . . . . . . . . 10 4 ∈ ℝ+
7756, 76rpdp2cl 32316 . . . . . . . . 9 14 ∈ ℝ+
7873, 77rpdp2cl 32316 . . . . . . . 8 414 ∈ ℝ+
7956, 78rpdpcl 32337 . . . . . . 7 (1.414) ∈ ℝ+
8079a1i 11 . . . . . 6 (πœ‘ β†’ (1.414) ∈ ℝ+)
8180rpred 13021 . . . . 5 (πœ‘ β†’ (1.414) ∈ ℝ)
8272, 81remulcld 11249 . . . 4 (πœ‘ β†’ (((1.079955)↑2) Β· (1.414)) ∈ ℝ)
83 fveq1 6890 . . . . . . . . . 10 (𝑑 = 𝑐 β†’ (π‘‘β€˜0) = (π‘β€˜0))
8483eleq1d 2817 . . . . . . . . 9 (𝑑 = 𝑐 β†’ ((π‘‘β€˜0) ∈ (𝑂 ∩ β„™) ↔ (π‘β€˜0) ∈ (𝑂 ∩ β„™)))
8584notbid 318 . . . . . . . 8 (𝑑 = 𝑐 β†’ (Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™) ↔ Β¬ (π‘β€˜0) ∈ (𝑂 ∩ β„™)))
8685cbvrabv 3441 . . . . . . 7 {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} = {𝑐 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘β€˜0) ∈ (𝑂 ∩ β„™)}
8786ssrab3 4080 . . . . . 6 {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} βŠ† (β„•(reprβ€˜3)𝑁)
88 ssfi 9177 . . . . . 6 (((β„•(reprβ€˜3)𝑁) ∈ Fin ∧ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} βŠ† (β„•(reprβ€˜3)𝑁)) β†’ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ∈ Fin)
896, 87, 88sylancl 585 . . . . 5 (πœ‘ β†’ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ∈ Fin)
909a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ Ξ›:β„•βŸΆβ„)
91 ssidd 4005 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ β„• βŠ† β„•)
9212adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ 𝑁 ∈ β„€)
933a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ 3 ∈ β„•0)
9487a1i 11 . . . . . . . . . 10 (πœ‘ β†’ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} βŠ† (β„•(reprβ€˜3)𝑁))
9594sselda 3982 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ 𝑛 ∈ (β„•(reprβ€˜3)𝑁))
9691, 92, 93, 95reprf 33923 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ 𝑛:(0..^3)βŸΆβ„•)
9721a1i 11 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ 0 ∈ (0..^3))
9896, 97ffvelcdmd 7087 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ (π‘›β€˜0) ∈ β„•)
9990, 98ffvelcdmd 7087 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ (Ξ›β€˜(π‘›β€˜0)) ∈ ℝ)
10033a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ 1 ∈ (0..^3))
10196, 100ffvelcdmd 7087 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ (π‘›β€˜1) ∈ β„•)
10290, 101ffvelcdmd 7087 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ (Ξ›β€˜(π‘›β€˜1)) ∈ ℝ)
10344a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ 2 ∈ (0..^3))
10496, 103ffvelcdmd 7087 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ (π‘›β€˜2) ∈ β„•)
10590, 104ffvelcdmd 7087 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ (Ξ›β€˜(π‘›β€˜2)) ∈ ℝ)
106102, 105remulcld 11249 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2))) ∈ ℝ)
10799, 106remulcld 11249 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))) ∈ ℝ)
10889, 107fsumrecl 15685 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))) ∈ ℝ)
10982, 108remulcld 11249 . . 3 (πœ‘ β†’ ((((1.079955)↑2) Β· (1.414)) Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2))))) ∈ ℝ)
11055, 109remulcld 11249 . 2 (πœ‘ β†’ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))))) ∈ ℝ)
111 4re 12301 . . . . . . . . . 10 4 ∈ ℝ
112 8re 12313 . . . . . . . . . 10 8 ∈ ℝ
113111, 112pm3.2i 470 . . . . . . . . 9 (4 ∈ ℝ ∧ 8 ∈ ℝ)
114 dp2cl 32314 . . . . . . . . 9 ((4 ∈ ℝ ∧ 8 ∈ ℝ) β†’ 48 ∈ ℝ)
115113, 114ax-mp 5 . . . . . . . 8 48 ∈ ℝ
11654, 115pm3.2i 470 . . . . . . 7 (3 ∈ ℝ ∧ 48 ∈ ℝ)
117 dp2cl 32314 . . . . . . 7 ((3 ∈ ℝ ∧ 48 ∈ ℝ) β†’ 348 ∈ ℝ)
118116, 117ax-mp 5 . . . . . 6 348 ∈ ℝ
119 dpcl 32325 . . . . . 6 ((7 ∈ β„•0 ∧ 348 ∈ ℝ) β†’ (7.348) ∈ ℝ)
12058, 118, 119mp2an 689 . . . . 5 (7.348) ∈ ℝ
121120a1i 11 . . . 4 (πœ‘ β†’ (7.348) ∈ ℝ)
1221nnrpd 13019 . . . . . 6 (πœ‘ β†’ 𝑁 ∈ ℝ+)
123122relogcld 26368 . . . . 5 (πœ‘ β†’ (logβ€˜π‘) ∈ ℝ)
1241nnred 12232 . . . . . 6 (πœ‘ β†’ 𝑁 ∈ ℝ)
125122rpge0d 13025 . . . . . 6 (πœ‘ β†’ 0 ≀ 𝑁)
126124, 125resqrtcld 15369 . . . . 5 (πœ‘ β†’ (βˆšβ€˜π‘) ∈ ℝ)
127122rpsqrtcld 15363 . . . . . 6 (πœ‘ β†’ (βˆšβ€˜π‘) ∈ ℝ+)
128127rpne0d 13026 . . . . 5 (πœ‘ β†’ (βˆšβ€˜π‘) β‰  0)
129123, 126, 128redivcld 12047 . . . 4 (πœ‘ β†’ ((logβ€˜π‘) / (βˆšβ€˜π‘)) ∈ ℝ)
130121, 129remulcld 11249 . . 3 (πœ‘ β†’ ((7.348) Β· ((logβ€˜π‘) / (βˆšβ€˜π‘))) ∈ ℝ)
131124resqcld 14095 . . 3 (πœ‘ β†’ (𝑁↑2) ∈ ℝ)
132130, 131remulcld 11249 . 2 (πœ‘ β†’ (((7.348) Β· ((logβ€˜π‘) / (βˆšβ€˜π‘))) Β· (𝑁↑2)) ∈ ℝ)
133 0re 11221 . . . . . . . . . . 11 0 ∈ ℝ
134 7re 12310 . . . . . . . . . . . . 13 7 ∈ ℝ
135 9re 12316 . . . . . . . . . . . . . . 15 9 ∈ ℝ
136 5re 12304 . . . . . . . . . . . . . . . . . . 19 5 ∈ ℝ
137136, 136pm3.2i 470 . . . . . . . . . . . . . . . . . 18 (5 ∈ ℝ ∧ 5 ∈ ℝ)
138 dp2cl 32314 . . . . . . . . . . . . . . . . . 18 ((5 ∈ ℝ ∧ 5 ∈ ℝ) β†’ 55 ∈ ℝ)
139137, 138ax-mp 5 . . . . . . . . . . . . . . . . 17 55 ∈ ℝ
140135, 139pm3.2i 470 . . . . . . . . . . . . . . . 16 (9 ∈ ℝ ∧ 55 ∈ ℝ)
141 dp2cl 32314 . . . . . . . . . . . . . . . 16 ((9 ∈ ℝ ∧ 55 ∈ ℝ) β†’ 955 ∈ ℝ)
142140, 141ax-mp 5 . . . . . . . . . . . . . . 15 955 ∈ ℝ
143135, 142pm3.2i 470 . . . . . . . . . . . . . 14 (9 ∈ ℝ ∧ 955 ∈ ℝ)
144 dp2cl 32314 . . . . . . . . . . . . . 14 ((9 ∈ ℝ ∧ 955 ∈ ℝ) β†’ 9955 ∈ ℝ)
145143, 144ax-mp 5 . . . . . . . . . . . . 13 9955 ∈ ℝ
146134, 145pm3.2i 470 . . . . . . . . . . . 12 (7 ∈ ℝ ∧ 9955 ∈ ℝ)
147 dp2cl 32314 . . . . . . . . . . . 12 ((7 ∈ ℝ ∧ 9955 ∈ ℝ) β†’ 79955 ∈ ℝ)
148146, 147ax-mp 5 . . . . . . . . . . 11 79955 ∈ ℝ
149133, 148pm3.2i 470 . . . . . . . . . 10 (0 ∈ ℝ ∧ 79955 ∈ ℝ)
150 dp2cl 32314 . . . . . . . . . 10 ((0 ∈ ℝ ∧ 79955 ∈ ℝ) β†’ 079955 ∈ ℝ)
151149, 150ax-mp 5 . . . . . . . . 9 079955 ∈ ℝ
152 dpcl 32325 . . . . . . . . 9 ((1 ∈ β„•0 ∧ 079955 ∈ ℝ) β†’ (1.079955) ∈ ℝ)
15356, 151, 152mp2an 689 . . . . . . . 8 (1.079955) ∈ ℝ
154153a1i 11 . . . . . . 7 (πœ‘ β†’ (1.079955) ∈ ℝ)
155154resqcld 14095 . . . . . 6 (πœ‘ β†’ ((1.079955)↑2) ∈ ℝ)
156 1re 11219 . . . . . . . . . . . 12 1 ∈ ℝ
157156, 111pm3.2i 470 . . . . . . . . . . 11 (1 ∈ ℝ ∧ 4 ∈ ℝ)
158 dp2cl 32314 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 4 ∈ ℝ) β†’ 14 ∈ ℝ)
159157, 158ax-mp 5 . . . . . . . . . 10 14 ∈ ℝ
160111, 159pm3.2i 470 . . . . . . . . 9 (4 ∈ ℝ ∧ 14 ∈ ℝ)
161 dp2cl 32314 . . . . . . . . 9 ((4 ∈ ℝ ∧ 14 ∈ ℝ) β†’ 414 ∈ ℝ)
162160, 161ax-mp 5 . . . . . . . 8 414 ∈ ℝ
163 dpcl 32325 . . . . . . . 8 ((1 ∈ β„•0 ∧ 414 ∈ ℝ) β†’ (1.414) ∈ ℝ)
16456, 162, 163mp2an 689 . . . . . . 7 (1.414) ∈ ℝ
165164a1i 11 . . . . . 6 (πœ‘ β†’ (1.414) ∈ ℝ)
166155, 165remulcld 11249 . . . . 5 (πœ‘ β†’ (((1.079955)↑2) Β· (1.414)) ∈ ℝ)
16736, 47remulcld 11249 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2))) ∈ ℝ)
16824, 167remulcld 11249 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))) ∈ ℝ)
1698, 168fsumrecl 15685 . . . . 5 (πœ‘ β†’ Σ𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))) ∈ ℝ)
170166, 169remulcld 11249 . . . 4 (πœ‘ β†’ ((((1.079955)↑2) Β· (1.414)) Β· Σ𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2))))) ∈ ℝ)
17155, 108remulcld 11249 . . . . 5 (πœ‘ β†’ (3 Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2))))) ∈ ℝ)
172166, 171remulcld 11249 . . . 4 (πœ‘ β†’ ((((1.079955)↑2) Β· (1.414)) Β· (3 Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))))) ∈ ℝ)
173 hgt750leme.1 . . . . 5 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (πΎβ€˜π‘š) ≀ (1.079955))
174 hgt750leme.2 . . . . 5 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (π»β€˜π‘š) ≀ (1.414))
1758, 154, 165, 26, 37, 23, 35, 46, 173, 174hgt750lemf 33964 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))(((Ξ›β€˜(π‘›β€˜0)) Β· (π»β€˜(π‘›β€˜0))) Β· (((Ξ›β€˜(π‘›β€˜1)) Β· (πΎβ€˜(π‘›β€˜1))) Β· ((Ξ›β€˜(π‘›β€˜2)) Β· (πΎβ€˜(π‘›β€˜2))))) ≀ ((((1.079955)↑2) Β· (1.414)) Β· Σ𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2))))))
176 hgt750leme.o . . . . . 6 𝑂 = {𝑧 ∈ β„€ ∣ Β¬ 2 βˆ₯ 𝑧}
177 2re 12291 . . . . . . . 8 2 ∈ ℝ
178177a1i 11 . . . . . . 7 (πœ‘ β†’ 2 ∈ ℝ)
179 10nn0 12700 . . . . . . . . . 10 10 ∈ β„•0
180 2nn0 12494 . . . . . . . . . . 11 2 ∈ β„•0
181180, 58deccl 12697 . . . . . . . . . 10 27 ∈ β„•0
182179, 181nn0expcli 14059 . . . . . . . . 9 (10↑27) ∈ β„•0
183182nn0rei 12488 . . . . . . . 8 (10↑27) ∈ ℝ
184183a1i 11 . . . . . . 7 (πœ‘ β†’ (10↑27) ∈ ℝ)
185179numexp1 17015 . . . . . . . . . 10 (10↑1) = 10
186179nn0rei 12488 . . . . . . . . . 10 10 ∈ ℝ
187185, 186eqeltri 2828 . . . . . . . . 9 (10↑1) ∈ ℝ
188187a1i 11 . . . . . . . 8 (πœ‘ β†’ (10↑1) ∈ ℝ)
189 1nn 12228 . . . . . . . . . . 11 1 ∈ β„•
190 2lt9 12422 . . . . . . . . . . . 12 2 < 9
191177, 135, 190ltleii 11342 . . . . . . . . . . 11 2 ≀ 9
192189, 57, 180, 191declei 12718 . . . . . . . . . 10 2 ≀ 10
193192, 185breqtrri 5175 . . . . . . . . 9 2 ≀ (10↑1)
194193a1i 11 . . . . . . . 8 (πœ‘ β†’ 2 ≀ (10↑1))
195 1z 12597 . . . . . . . . . . . 12 1 ∈ β„€
196181nn0zi 12592 . . . . . . . . . . . 12 27 ∈ β„€
197186, 195, 1963pm3.2i 1338 . . . . . . . . . . 11 (10 ∈ ℝ ∧ 1 ∈ β„€ ∧ 27 ∈ β„€)
198 1lt10 12821 . . . . . . . . . . 11 1 < 10
199197, 198pm3.2i 470 . . . . . . . . . 10 ((10 ∈ ℝ ∧ 1 ∈ β„€ ∧ 27 ∈ β„€) ∧ 1 < 10)
200 2nn 12290 . . . . . . . . . . 11 2 ∈ β„•
201 1lt9 12423 . . . . . . . . . . . 12 1 < 9
202156, 135, 201ltleii 11342 . . . . . . . . . . 11 1 ≀ 9
203200, 58, 56, 202declei 12718 . . . . . . . . . 10 1 ≀ 27
204 leexp2 14141 . . . . . . . . . . 11 (((10 ∈ ℝ ∧ 1 ∈ β„€ ∧ 27 ∈ β„€) ∧ 1 < 10) β†’ (1 ≀ 27 ↔ (10↑1) ≀ (10↑27)))
205204biimpa 476 . . . . . . . . . 10 ((((10 ∈ ℝ ∧ 1 ∈ β„€ ∧ 27 ∈ β„€) ∧ 1 < 10) ∧ 1 ≀ 27) β†’ (10↑1) ≀ (10↑27))
206199, 203, 205mp2an 689 . . . . . . . . 9 (10↑1) ≀ (10↑27)
207206a1i 11 . . . . . . . 8 (πœ‘ β†’ (10↑1) ≀ (10↑27))
208178, 188, 184, 194, 207letrd 11376 . . . . . . 7 (πœ‘ β†’ 2 ≀ (10↑27))
209 hgt750leme.0 . . . . . . 7 (πœ‘ β†’ (10↑27) ≀ 𝑁)
210178, 184, 124, 208, 209letrd 11376 . . . . . 6 (πœ‘ β†’ 2 ≀ 𝑁)
211 eqid 2731 . . . . . 6 (𝑒 ∈ {𝑐 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘β€˜π‘Ž) ∈ (𝑂 ∩ β„™)} ↦ (𝑒 ∘ if(π‘Ž = 0, ( I β†Ύ (0..^3)), ((pmTrspβ€˜(0..^3))β€˜{π‘Ž, 0})))) = (𝑒 ∈ {𝑐 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘β€˜π‘Ž) ∈ (𝑂 ∩ β„™)} ↦ (𝑒 ∘ if(π‘Ž = 0, ( I β†Ύ (0..^3)), ((pmTrspβ€˜(0..^3))β€˜{π‘Ž, 0}))))
212176, 1, 210, 86, 211hgt750lema 33968 . . . . 5 (πœ‘ β†’ Σ𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))) ≀ (3 Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2))))))
213 2z 12599 . . . . . . . . 9 2 ∈ β„€
214213a1i 11 . . . . . . . 8 (πœ‘ β†’ 2 ∈ β„€)
21570, 214rpexpcld 14215 . . . . . . 7 (πœ‘ β†’ ((1.079955)↑2) ∈ ℝ+)
216215, 80rpmulcld 13037 . . . . . 6 (πœ‘ β†’ (((1.079955)↑2) Β· (1.414)) ∈ ℝ+)
217169, 171, 216lemul2d 13065 . . . . 5 (πœ‘ β†’ (Σ𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))) ≀ (3 Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2))))) ↔ ((((1.079955)↑2) Β· (1.414)) Β· Σ𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2))))) ≀ ((((1.079955)↑2) Β· (1.414)) Β· (3 Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2))))))))
218212, 217mpbid 231 . . . 4 (πœ‘ β†’ ((((1.079955)↑2) Β· (1.414)) Β· Σ𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2))))) ≀ ((((1.079955)↑2) Β· (1.414)) Β· (3 Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))))))
21953, 170, 172, 175, 218letrd 11376 . . 3 (πœ‘ β†’ Σ𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))(((Ξ›β€˜(π‘›β€˜0)) Β· (π»β€˜(π‘›β€˜0))) Β· (((Ξ›β€˜(π‘›β€˜1)) Β· (πΎβ€˜(π‘›β€˜1))) Β· ((Ξ›β€˜(π‘›β€˜2)) Β· (πΎβ€˜(π‘›β€˜2))))) ≀ ((((1.079955)↑2) Β· (1.414)) Β· (3 Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))))))
220154recnd 11247 . . . . . 6 (πœ‘ β†’ (1.079955) ∈ β„‚)
221220sqcld 14114 . . . . 5 (πœ‘ β†’ ((1.079955)↑2) ∈ β„‚)
222165recnd 11247 . . . . 5 (πœ‘ β†’ (1.414) ∈ β„‚)
223221, 222mulcld 11239 . . . 4 (πœ‘ β†’ (((1.079955)↑2) Β· (1.414)) ∈ β„‚)
224 3cn 12298 . . . . 5 3 ∈ β„‚
225224a1i 11 . . . 4 (πœ‘ β†’ 3 ∈ β„‚)
226108recnd 11247 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))) ∈ β„‚)
227223, 225, 226mul12d 11428 . . 3 (πœ‘ β†’ ((((1.079955)↑2) Β· (1.414)) Β· (3 Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))))) = (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))))))
228219, 227breqtrd 5174 . 2 (πœ‘ β†’ Σ𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))(((Ξ›β€˜(π‘›β€˜0)) Β· (π»β€˜(π‘›β€˜0))) Β· (((Ξ›β€˜(π‘›β€˜1)) Β· (πΎβ€˜(π‘›β€˜1))) Β· ((Ξ›β€˜(π‘›β€˜2)) Β· (πΎβ€˜(π‘›β€˜2))))) ≀ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))))))
229 fzfi 13942 . . . . . . . . . . 11 (1...𝑁) ∈ Fin
230 diffi 9183 . . . . . . . . . . 11 ((1...𝑁) ∈ Fin β†’ ((1...𝑁) βˆ– β„™) ∈ Fin)
231229, 230ax-mp 5 . . . . . . . . . 10 ((1...𝑁) βˆ– β„™) ∈ Fin
232 snfi 9048 . . . . . . . . . 10 {2} ∈ Fin
233 unfi 9176 . . . . . . . . . 10 ((((1...𝑁) βˆ– β„™) ∈ Fin ∧ {2} ∈ Fin) β†’ (((1...𝑁) βˆ– β„™) βˆͺ {2}) ∈ Fin)
234231, 232, 233mp2an 689 . . . . . . . . 9 (((1...𝑁) βˆ– β„™) βˆͺ {2}) ∈ Fin
235234a1i 11 . . . . . . . 8 (πœ‘ β†’ (((1...𝑁) βˆ– β„™) βˆͺ {2}) ∈ Fin)
2369a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})) β†’ Ξ›:β„•βŸΆβ„)
237 fz1ssnn 13537 . . . . . . . . . . . . 13 (1...𝑁) βŠ† β„•
238237a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ (1...𝑁) βŠ† β„•)
239238ssdifssd 4142 . . . . . . . . . . 11 (πœ‘ β†’ ((1...𝑁) βˆ– β„™) βŠ† β„•)
240200a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ 2 ∈ β„•)
241240snssd 4812 . . . . . . . . . . 11 (πœ‘ β†’ {2} βŠ† β„•)
242239, 241unssd 4186 . . . . . . . . . 10 (πœ‘ β†’ (((1...𝑁) βˆ– β„™) βˆͺ {2}) βŠ† β„•)
243242sselda 3982 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})) β†’ 𝑖 ∈ β„•)
244236, 243ffvelcdmd 7087 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})) β†’ (Ξ›β€˜π‘–) ∈ ℝ)
245235, 244fsumrecl 15685 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) ∈ ℝ)
246 chpvalz 33939 . . . . . . . . 9 (𝑁 ∈ β„€ β†’ (Οˆβ€˜π‘) = Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))
24712, 246syl 17 . . . . . . . 8 (πœ‘ β†’ (Οˆβ€˜π‘) = Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))
248 chpf 26864 . . . . . . . . . 10 ψ:β„βŸΆβ„
249248a1i 11 . . . . . . . . 9 (πœ‘ β†’ ψ:β„βŸΆβ„)
250249, 124ffvelcdmd 7087 . . . . . . . 8 (πœ‘ β†’ (Οˆβ€˜π‘) ∈ ℝ)
251247, 250eqeltrrd 2833 . . . . . . 7 (πœ‘ β†’ Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—) ∈ ℝ)
252245, 251remulcld 11249 . . . . . 6 (πœ‘ β†’ (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—)) ∈ ℝ)
253123, 252remulcld 11249 . . . . 5 (πœ‘ β†’ ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))) ∈ ℝ)
25482, 253remulcld 11249 . . . 4 (πœ‘ β†’ ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—)))) ∈ ℝ)
25555, 254remulcld 11249 . . 3 (πœ‘ β†’ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))))) ∈ ℝ)
256176, 1, 210, 86hgt750lemb 33967 . . . . 5 (πœ‘ β†’ Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))) ≀ ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))))
257108, 253, 216lemul2d 13065 . . . . 5 (πœ‘ β†’ (Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))) ≀ ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))) ↔ ((((1.079955)↑2) Β· (1.414)) Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2))))) ≀ ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))))))
258256, 257mpbid 231 . . . 4 (πœ‘ β†’ ((((1.079955)↑2) Β· (1.414)) Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2))))) ≀ ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—)))))
259 3rp 12985 . . . . . 6 3 ∈ ℝ+
260259a1i 11 . . . . 5 (πœ‘ β†’ 3 ∈ ℝ+)
261109, 254, 260lemul2d 13065 . . . 4 (πœ‘ β†’ (((((1.079955)↑2) Β· (1.414)) Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2))))) ≀ ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—)))) ↔ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))))) ≀ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—)))))))
262258, 261mpbid 231 . . 3 (πœ‘ β†’ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))))) ≀ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))))))
263 6re 12307 . . . . . . . . . . . . . . . . 17 6 ∈ ℝ
264263, 54pm3.2i 470 . . . . . . . . . . . . . . . 16 (6 ∈ ℝ ∧ 3 ∈ ℝ)
265 dp2cl 32314 . . . . . . . . . . . . . . . 16 ((6 ∈ ℝ ∧ 3 ∈ ℝ) β†’ 63 ∈ ℝ)
266264, 265ax-mp 5 . . . . . . . . . . . . . . 15 63 ∈ ℝ
267177, 266pm3.2i 470 . . . . . . . . . . . . . 14 (2 ∈ ℝ ∧ 63 ∈ ℝ)
268 dp2cl 32314 . . . . . . . . . . . . . 14 ((2 ∈ ℝ ∧ 63 ∈ ℝ) β†’ 263 ∈ ℝ)
269267, 268ax-mp 5 . . . . . . . . . . . . 13 263 ∈ ℝ
270111, 269pm3.2i 470 . . . . . . . . . . . 12 (4 ∈ ℝ ∧ 263 ∈ ℝ)
271 dp2cl 32314 . . . . . . . . . . . 12 ((4 ∈ ℝ ∧ 263 ∈ ℝ) β†’ 4263 ∈ ℝ)
272270, 271ax-mp 5 . . . . . . . . . . 11 4263 ∈ ℝ
273 dpcl 32325 . . . . . . . . . . 11 ((1 ∈ β„•0 ∧ 4263 ∈ ℝ) β†’ (1.4263) ∈ ℝ)
27456, 272, 273mp2an 689 . . . . . . . . . 10 (1.4263) ∈ ℝ
275274a1i 11 . . . . . . . . 9 (πœ‘ β†’ (1.4263) ∈ ℝ)
276275, 126remulcld 11249 . . . . . . . 8 (πœ‘ β†’ ((1.4263) Β· (βˆšβ€˜π‘)) ∈ ℝ)
277112, 54pm3.2i 470 . . . . . . . . . . . . . . . . . 18 (8 ∈ ℝ ∧ 3 ∈ ℝ)
278 dp2cl 32314 . . . . . . . . . . . . . . . . . 18 ((8 ∈ ℝ ∧ 3 ∈ ℝ) β†’ 83 ∈ ℝ)
279277, 278ax-mp 5 . . . . . . . . . . . . . . . . 17 83 ∈ ℝ
280112, 279pm3.2i 470 . . . . . . . . . . . . . . . 16 (8 ∈ ℝ ∧ 83 ∈ ℝ)
281 dp2cl 32314 . . . . . . . . . . . . . . . 16 ((8 ∈ ℝ ∧ 83 ∈ ℝ) β†’ 883 ∈ ℝ)
282280, 281ax-mp 5 . . . . . . . . . . . . . . 15 883 ∈ ℝ
28354, 282pm3.2i 470 . . . . . . . . . . . . . 14 (3 ∈ ℝ ∧ 883 ∈ ℝ)
284 dp2cl 32314 . . . . . . . . . . . . . 14 ((3 ∈ ℝ ∧ 883 ∈ ℝ) β†’ 3883 ∈ ℝ)
285283, 284ax-mp 5 . . . . . . . . . . . . 13 3883 ∈ ℝ
286133, 285pm3.2i 470 . . . . . . . . . . . 12 (0 ∈ ℝ ∧ 3883 ∈ ℝ)
287 dp2cl 32314 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ 3883 ∈ ℝ) β†’ 03883 ∈ ℝ)
288286, 287ax-mp 5 . . . . . . . . . . 11 03883 ∈ ℝ
289 dpcl 32325 . . . . . . . . . . 11 ((1 ∈ β„•0 ∧ 03883 ∈ ℝ) β†’ (1.03883) ∈ ℝ)
29056, 288, 289mp2an 689 . . . . . . . . . 10 (1.03883) ∈ ℝ
291290a1i 11 . . . . . . . . 9 (πœ‘ β†’ (1.03883) ∈ ℝ)
292291, 124remulcld 11249 . . . . . . . 8 (πœ‘ β†’ ((1.03883) Β· 𝑁) ∈ ℝ)
293276, 292remulcld 11249 . . . . . . 7 (πœ‘ β†’ (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁)) ∈ ℝ)
294123, 293remulcld 11249 . . . . . 6 (πœ‘ β†’ ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))) ∈ ℝ)
29582, 294remulcld 11249 . . . . 5 (πœ‘ β†’ ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁)))) ∈ ℝ)
29655, 295remulcld 11249 . . . 4 (πœ‘ β†’ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))))) ∈ ℝ)
297 vmage0 26862 . . . . . . . . . . 11 (𝑖 ∈ β„• β†’ 0 ≀ (Ξ›β€˜π‘–))
298243, 297syl 17 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})) β†’ 0 ≀ (Ξ›β€˜π‘–))
299235, 244, 298fsumge0 15746 . . . . . . . . 9 (πœ‘ β†’ 0 ≀ Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–))
3001, 209hgt750lemd 33959 . . . . . . . . 9 (πœ‘ β†’ Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) < ((1.4263) Β· (βˆšβ€˜π‘)))
301 fzfid 13943 . . . . . . . . . 10 (πœ‘ β†’ (1...𝑁) ∈ Fin)
3029a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ (1...𝑁)) β†’ Ξ›:β„•βŸΆβ„)
303238sselda 3982 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ (1...𝑁)) β†’ 𝑗 ∈ β„•)
304302, 303ffvelcdmd 7087 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (1...𝑁)) β†’ (Ξ›β€˜π‘—) ∈ ℝ)
305 vmage0 26862 . . . . . . . . . . 11 (𝑗 ∈ β„• β†’ 0 ≀ (Ξ›β€˜π‘—))
306303, 305syl 17 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (1...𝑁)) β†’ 0 ≀ (Ξ›β€˜π‘—))
307301, 304, 306fsumge0 15746 . . . . . . . . 9 (πœ‘ β†’ 0 ≀ Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))
3081hgt750lemc 33958 . . . . . . . . 9 (πœ‘ β†’ Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—) < ((1.03883) Β· 𝑁))
309245, 276, 251, 292, 299, 300, 307, 308ltmul12ad 12160 . . . . . . . 8 (πœ‘ β†’ (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—)) < (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁)))
310252, 293, 309ltled 11367 . . . . . . 7 (πœ‘ β†’ (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—)) ≀ (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁)))
311156a1i 11 . . . . . . . . . 10 (πœ‘ β†’ 1 ∈ ℝ)
312 1lt2 12388 . . . . . . . . . . 11 1 < 2
313312a1i 11 . . . . . . . . . 10 (πœ‘ β†’ 1 < 2)
314311, 178, 124, 313, 210ltletrd 11379 . . . . . . . . 9 (πœ‘ β†’ 1 < 𝑁)
315124, 314rplogcld 26374 . . . . . . . 8 (πœ‘ β†’ (logβ€˜π‘) ∈ ℝ+)
316252, 293, 315lemul2d 13065 . . . . . . 7 (πœ‘ β†’ ((Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—)) ≀ (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁)) ↔ ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))) ≀ ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁)))))
317310, 316mpbid 231 . . . . . 6 (πœ‘ β†’ ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))) ≀ ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))))
318253, 294, 216lemul2d 13065 . . . . . 6 (πœ‘ β†’ (((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))) ≀ ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))) ↔ ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—)))) ≀ ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))))))
319317, 318mpbid 231 . . . . 5 (πœ‘ β†’ ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—)))) ≀ ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁)))))
320254, 295, 260lemul2d 13065 . . . . 5 (πœ‘ β†’ (((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—)))) ≀ ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁)))) ↔ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))))) ≀ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁)))))))
321319, 320mpbid 231 . . . 4 (πœ‘ β†’ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))))) ≀ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))))))
322153resqcli 14155 . . . . . . . . . 10 ((1.079955)↑2) ∈ ℝ
323322, 164remulcli 11235 . . . . . . . . 9 (((1.079955)↑2) Β· (1.414)) ∈ ℝ
324274, 290remulcli 11235 . . . . . . . . 9 ((1.4263) Β· (1.03883)) ∈ ℝ
325323, 324remulcli 11235 . . . . . . . 8 ((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883))) ∈ ℝ
32654, 325remulcli 11235 . . . . . . 7 (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883)))) ∈ ℝ
327 hgt750lem2 33963 . . . . . . 7 (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883)))) < (7.348)
328326, 120, 327ltleii 11342 . . . . . 6 (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883)))) ≀ (7.348)
329326a1i 11 . . . . . . 7 (πœ‘ β†’ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883)))) ∈ ℝ)
330315, 127rpdivcld 13038 . . . . . . . 8 (πœ‘ β†’ ((logβ€˜π‘) / (βˆšβ€˜π‘)) ∈ ℝ+)
331122, 214rpexpcld 14215 . . . . . . . 8 (πœ‘ β†’ (𝑁↑2) ∈ ℝ+)
332330, 331rpmulcld 13037 . . . . . . 7 (πœ‘ β†’ (((logβ€˜π‘) / (βˆšβ€˜π‘)) Β· (𝑁↑2)) ∈ ℝ+)
333329, 121, 332lemul1d 13064 . . . . . 6 (πœ‘ β†’ ((3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883)))) ≀ (7.348) ↔ ((3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883)))) Β· (((logβ€˜π‘) / (βˆšβ€˜π‘)) Β· (𝑁↑2))) ≀ ((7.348) Β· (((logβ€˜π‘) / (βˆšβ€˜π‘)) Β· (𝑁↑2)))))
334328, 333mpbii 232 . . . . 5 (πœ‘ β†’ ((3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883)))) Β· (((logβ€˜π‘) / (βˆšβ€˜π‘)) Β· (𝑁↑2))) ≀ ((7.348) Β· (((logβ€˜π‘) / (βˆšβ€˜π‘)) Β· (𝑁↑2))))
335275recnd 11247 . . . . . . . . . . . . . 14 (πœ‘ β†’ (1.4263) ∈ β„‚)
336126recnd 11247 . . . . . . . . . . . . . 14 (πœ‘ β†’ (βˆšβ€˜π‘) ∈ β„‚)
337291recnd 11247 . . . . . . . . . . . . . 14 (πœ‘ β†’ (1.03883) ∈ β„‚)
338124recnd 11247 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑁 ∈ β„‚)
339335, 336, 337, 338mul4d 11431 . . . . . . . . . . . . 13 (πœ‘ β†’ (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁)) = (((1.4263) Β· (1.03883)) Β· ((βˆšβ€˜π‘) Β· 𝑁)))
340339oveq2d 7428 . . . . . . . . . . . 12 (πœ‘ β†’ ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))) = ((logβ€˜π‘) Β· (((1.4263) Β· (1.03883)) Β· ((βˆšβ€˜π‘) Β· 𝑁))))
341123recnd 11247 . . . . . . . . . . . . 13 (πœ‘ β†’ (logβ€˜π‘) ∈ β„‚)
342335, 337mulcld 11239 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((1.4263) Β· (1.03883)) ∈ β„‚)
343336, 338mulcld 11239 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((βˆšβ€˜π‘) Β· 𝑁) ∈ β„‚)
344342, 343mulcld 11239 . . . . . . . . . . . . 13 (πœ‘ β†’ (((1.4263) Β· (1.03883)) Β· ((βˆšβ€˜π‘) Β· 𝑁)) ∈ β„‚)
345341, 344mulcomd 11240 . . . . . . . . . . . 12 (πœ‘ β†’ ((logβ€˜π‘) Β· (((1.4263) Β· (1.03883)) Β· ((βˆšβ€˜π‘) Β· 𝑁))) = ((((1.4263) Β· (1.03883)) Β· ((βˆšβ€˜π‘) Β· 𝑁)) Β· (logβ€˜π‘)))
346340, 345eqtrd 2771 . . . . . . . . . . 11 (πœ‘ β†’ ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))) = ((((1.4263) Β· (1.03883)) Β· ((βˆšβ€˜π‘) Β· 𝑁)) Β· (logβ€˜π‘)))
347342, 343, 341mulassd 11242 . . . . . . . . . . 11 (πœ‘ β†’ ((((1.4263) Β· (1.03883)) Β· ((βˆšβ€˜π‘) Β· 𝑁)) Β· (logβ€˜π‘)) = (((1.4263) Β· (1.03883)) Β· (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘))))
348346, 347eqtrd 2771 . . . . . . . . . 10 (πœ‘ β†’ ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))) = (((1.4263) Β· (1.03883)) Β· (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘))))
349348oveq2d 7428 . . . . . . . . 9 (πœ‘ β†’ ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁)))) = ((((1.079955)↑2) Β· (1.414)) Β· (((1.4263) Β· (1.03883)) Β· (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘)))))
35082recnd 11247 . . . . . . . . . 10 (πœ‘ β†’ (((1.079955)↑2) Β· (1.414)) ∈ β„‚)
351343, 341mulcld 11239 . . . . . . . . . 10 (πœ‘ β†’ (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘)) ∈ β„‚)
352350, 342, 351mulassd 11242 . . . . . . . . 9 (πœ‘ β†’ (((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883))) Β· (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘))) = ((((1.079955)↑2) Β· (1.414)) Β· (((1.4263) Β· (1.03883)) Β· (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘)))))
353349, 352eqtr4d 2774 . . . . . . . 8 (πœ‘ β†’ ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁)))) = (((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883))) Β· (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘))))
354353oveq2d 7428 . . . . . . 7 (πœ‘ β†’ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))))) = (3 Β· (((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883))) Β· (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘)))))
35555recnd 11247 . . . . . . . 8 (πœ‘ β†’ 3 ∈ β„‚)
356350, 342mulcld 11239 . . . . . . . 8 (πœ‘ β†’ ((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883))) ∈ β„‚)
357355, 356, 351mulassd 11242 . . . . . . 7 (πœ‘ β†’ ((3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883)))) Β· (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘))) = (3 Β· (((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883))) Β· (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘)))))
358354, 357eqtr4d 2774 . . . . . 6 (πœ‘ β†’ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))))) = ((3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883)))) Β· (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘))))
359131recnd 11247 . . . . . . . . 9 (πœ‘ β†’ (𝑁↑2) ∈ β„‚)
360341, 336, 359, 128div32d 12018 . . . . . . . 8 (πœ‘ β†’ (((logβ€˜π‘) / (βˆšβ€˜π‘)) Β· (𝑁↑2)) = ((logβ€˜π‘) Β· ((𝑁↑2) / (βˆšβ€˜π‘))))
361359, 336, 128divcld 11995 . . . . . . . . 9 (πœ‘ β†’ ((𝑁↑2) / (βˆšβ€˜π‘)) ∈ β„‚)
362341, 361mulcomd 11240 . . . . . . . 8 (πœ‘ β†’ ((logβ€˜π‘) Β· ((𝑁↑2) / (βˆšβ€˜π‘))) = (((𝑁↑2) / (βˆšβ€˜π‘)) Β· (logβ€˜π‘)))
363338sqvald 14113 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑁↑2) = (𝑁 Β· 𝑁))
364363oveq1d 7427 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑁↑2) / (βˆšβ€˜π‘)) = ((𝑁 Β· 𝑁) / (βˆšβ€˜π‘)))
365338, 338, 336, 128divassd 12030 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑁 Β· 𝑁) / (βˆšβ€˜π‘)) = (𝑁 Β· (𝑁 / (βˆšβ€˜π‘))))
366 divsqrtid 33905 . . . . . . . . . . . . 13 (𝑁 ∈ ℝ+ β†’ (𝑁 / (βˆšβ€˜π‘)) = (βˆšβ€˜π‘))
367122, 366syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑁 / (βˆšβ€˜π‘)) = (βˆšβ€˜π‘))
368367oveq2d 7428 . . . . . . . . . . 11 (πœ‘ β†’ (𝑁 Β· (𝑁 / (βˆšβ€˜π‘))) = (𝑁 Β· (βˆšβ€˜π‘)))
369364, 365, 3683eqtrd 2775 . . . . . . . . . 10 (πœ‘ β†’ ((𝑁↑2) / (βˆšβ€˜π‘)) = (𝑁 Β· (βˆšβ€˜π‘)))
370338, 336mulcomd 11240 . . . . . . . . . 10 (πœ‘ β†’ (𝑁 Β· (βˆšβ€˜π‘)) = ((βˆšβ€˜π‘) Β· 𝑁))
371369, 370eqtrd 2771 . . . . . . . . 9 (πœ‘ β†’ ((𝑁↑2) / (βˆšβ€˜π‘)) = ((βˆšβ€˜π‘) Β· 𝑁))
372371oveq1d 7427 . . . . . . . 8 (πœ‘ β†’ (((𝑁↑2) / (βˆšβ€˜π‘)) Β· (logβ€˜π‘)) = (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘)))
373360, 362, 3723eqtrrd 2776 . . . . . . 7 (πœ‘ β†’ (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘)) = (((logβ€˜π‘) / (βˆšβ€˜π‘)) Β· (𝑁↑2)))
374373oveq2d 7428 . . . . . 6 (πœ‘ β†’ ((3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883)))) Β· (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘))) = ((3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883)))) Β· (((logβ€˜π‘) / (βˆšβ€˜π‘)) Β· (𝑁↑2))))
375358, 374eqtrd 2771 . . . . 5 (πœ‘ β†’ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))))) = ((3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883)))) Β· (((logβ€˜π‘) / (βˆšβ€˜π‘)) Β· (𝑁↑2))))
376121recnd 11247 . . . . . 6 (πœ‘ β†’ (7.348) ∈ β„‚)
377129recnd 11247 . . . . . 6 (πœ‘ β†’ ((logβ€˜π‘) / (βˆšβ€˜π‘)) ∈ β„‚)
378376, 377, 359mulassd 11242 . . . . 5 (πœ‘ β†’ (((7.348) Β· ((logβ€˜π‘) / (βˆšβ€˜π‘))) Β· (𝑁↑2)) = ((7.348) Β· (((logβ€˜π‘) / (βˆšβ€˜π‘)) Β· (𝑁↑2))))
379334, 375, 3783brtr4d 5180 . . . 4 (πœ‘ β†’ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))))) ≀ (((7.348) Β· ((logβ€˜π‘) / (βˆšβ€˜π‘))) Β· (𝑁↑2)))
380255, 296, 132, 321, 379letrd 11376 . . 3 (πœ‘ β†’ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))))) ≀ (((7.348) Β· ((logβ€˜π‘) / (βˆšβ€˜π‘))) Β· (𝑁↑2)))
381110, 255, 132, 262, 380letrd 11376 . 2 (πœ‘ β†’ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))))) ≀ (((7.348) Β· ((logβ€˜π‘) / (βˆšβ€˜π‘))) Β· (𝑁↑2)))
38253, 110, 132, 228, 381letrd 11376 1 (πœ‘ β†’ Σ𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))(((Ξ›β€˜(π‘›β€˜0)) Β· (π»β€˜(π‘›β€˜0))) Β· (((Ξ›β€˜(π‘›β€˜1)) Β· (πΎβ€˜(π‘›β€˜1))) Β· ((Ξ›β€˜(π‘›β€˜2)) Β· (πΎβ€˜(π‘›β€˜2))))) ≀ (((7.348) Β· ((logβ€˜π‘) / (βˆšβ€˜π‘))) Β· (𝑁↑2)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  {crab 3431   βˆ– cdif 3945   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  ifcif 4528  {csn 4628  {cpr 4630  {ctp 4632   class class class wbr 5148   ↦ cmpt 5231   I cid 5573   β†Ύ cres 5678   ∘ ccom 5680  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7412  Fincfn 8943  β„‚cc 11112  β„cr 11113  0cc0 11114  1c1 11115   Β· cmul 11119  +∞cpnf 11250   < clt 11253   ≀ cle 11254   / cdiv 11876  β„•cn 12217  2c2 12272  3c3 12273  4c4 12274  5c5 12275  6c6 12276  7c7 12277  8c8 12278  9c9 12279  β„•0cn0 12477  β„€cz 12563  cdc 12682  β„+crp 12979  [,)cico 13331  ...cfz 13489  ..^cfzo 13632  β†‘cexp 14032  βˆšcsqrt 15185  Ξ£csu 15637   βˆ₯ cdvds 16202  β„™cprime 16613  pmTrspcpmtr 19351  logclog 26300  Ξ›cvma 26833  Οˆcchp 26834  cdp2 32305  .cdp 32322  reprcrepr 33919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-reg 9591  ax-inf2 9640  ax-ac2 10462  ax-cnex 11170  ax-resscn 11171  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-mulcom 11178  ax-addass 11179  ax-mulass 11180  ax-distr 11181  ax-i2m1 11182  ax-1ne0 11183  ax-1rid 11184  ax-rnegex 11185  ax-rrecex 11186  ax-cnre 11187  ax-pre-lttri 11188  ax-pre-lttrn 11189  ax-pre-ltadd 11190  ax-pre-mulgt0 11191  ax-pre-sup 11192  ax-addf 11193  ax-mulf 11194  ax-ros335 33956  ax-ros336 33957
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7674  df-om 7860  df-1st 7979  df-2nd 7980  df-supp 8151  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-1o 8470  df-2o 8471  df-oadd 8474  df-er 8707  df-map 8826  df-pm 8827  df-ixp 8896  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-fsupp 9366  df-fi 9410  df-sup 9441  df-inf 9442  df-oi 9509  df-r1 9763  df-rank 9764  df-dju 9900  df-card 9938  df-ac 10115  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-div 11877  df-nn 12218  df-2 12280  df-3 12281  df-4 12282  df-5 12283  df-6 12284  df-7 12285  df-8 12286  df-9 12287  df-n0 12478  df-xnn0 12550  df-z 12564  df-dec 12683  df-uz 12828  df-q 12938  df-rp 12980  df-xneg 13097  df-xadd 13098  df-xmul 13099  df-ioo 13333  df-ioc 13334  df-ico 13335  df-icc 13336  df-fz 13490  df-fzo 13633  df-fl 13762  df-mod 13840  df-seq 13972  df-exp 14033  df-fac 14239  df-bc 14268  df-hash 14296  df-shft 15019  df-cj 15051  df-re 15052  df-im 15053  df-sqrt 15187  df-abs 15188  df-limsup 15420  df-clim 15437  df-rlim 15438  df-sum 15638  df-prod 15855  df-ef 16016  df-sin 16018  df-cos 16019  df-tan 16020  df-pi 16021  df-dvds 16203  df-gcd 16441  df-prm 16614  df-pc 16775  df-struct 17085  df-sets 17102  df-slot 17120  df-ndx 17132  df-base 17150  df-ress 17179  df-plusg 17215  df-mulr 17216  df-starv 17217  df-sca 17218  df-vsca 17219  df-ip 17220  df-tset 17221  df-ple 17222  df-ds 17224  df-unif 17225  df-hom 17226  df-cco 17227  df-rest 17373  df-topn 17374  df-0g 17392  df-gsum 17393  df-topgen 17394  df-pt 17395  df-prds 17398  df-xrs 17453  df-qtop 17458  df-imas 17459  df-xps 17461  df-mre 17535  df-mrc 17536  df-acs 17538  df-mgm 18566  df-sgrp 18645  df-mnd 18661  df-submnd 18707  df-mulg 18988  df-cntz 19223  df-pmtr 19352  df-cmn 19692  df-psmet 21137  df-xmet 21138  df-met 21139  df-bl 21140  df-mopn 21141  df-fbas 21142  df-fg 21143  df-cnfld 21146  df-top 22617  df-topon 22634  df-topsp 22656  df-bases 22670  df-cld 22744  df-ntr 22745  df-cls 22746  df-nei 22823  df-lp 22861  df-perf 22862  df-cn 22952  df-cnp 22953  df-haus 23040  df-cmp 23112  df-tx 23287  df-hmeo 23480  df-fil 23571  df-fm 23663  df-flim 23664  df-flf 23665  df-xms 24047  df-ms 24048  df-tms 24049  df-cncf 24619  df-limc 25616  df-dv 25617  df-ulm 26126  df-log 26302  df-atan 26609  df-cht 26838  df-vma 26839  df-chp 26840  df-dp2 32306  df-dp 32323  df-repr 33920
This theorem is referenced by:  tgoldbachgtde  33971
  Copyright terms: Public domain W3C validator