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 34159
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 12529 . . . . 5 (πœ‘ β†’ 𝑁 ∈ β„•0)
3 3nn0 12487 . . . . . 6 3 ∈ β„•0
43a1i 11 . . . . 5 (πœ‘ β†’ 3 ∈ β„•0)
5 ssidd 3997 . . . . 5 (πœ‘ β†’ β„• βŠ† β„•)
62, 4, 5reprfi2 34124 . . . 4 (πœ‘ β†’ (β„•(reprβ€˜3)𝑁) ∈ Fin)
7 diffi 9175 . . . 4 ((β„•(reprβ€˜3)𝑁) ∈ Fin β†’ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁)) ∈ Fin)
86, 7syl 17 . . 3 (πœ‘ β†’ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁)) ∈ Fin)
9 vmaf 26967 . . . . . . 7 Ξ›:β„•βŸΆβ„
109a1i 11 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ Ξ›:β„•βŸΆβ„)
11 ssidd 3997 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ β„• βŠ† β„•)
121nnzd 12582 . . . . . . . . 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 3952 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 𝑛 ∈ (β„•(reprβ€˜3)𝑁))
1711, 13, 14, 16reprf 34113 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 𝑛:(0..^3)βŸΆβ„•)
18 c0ex 11205 . . . . . . . . . 10 0 ∈ V
1918tpid1 4764 . . . . . . . . 9 0 ∈ {0, 1, 2}
20 fzo0to3tp 13715 . . . . . . . . 9 (0..^3) = {0, 1, 2}
2119, 20eleqtrri 2824 . . . . . . . 8 0 ∈ (0..^3)
2221a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 0 ∈ (0..^3))
2317, 22ffvelcdmd 7077 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (π‘›β€˜0) ∈ β„•)
2410, 23ffvelcdmd 7077 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (Ξ›β€˜(π‘›β€˜0)) ∈ ℝ)
25 rge0ssre 13430 . . . . . 6 (0[,)+∞) βŠ† ℝ
26 hgt750leme.h . . . . . . . 8 (πœ‘ β†’ 𝐻:β„•βŸΆ(0[,)+∞))
2726adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 𝐻:β„•βŸΆ(0[,)+∞))
2827, 23ffvelcdmd 7077 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (π»β€˜(π‘›β€˜0)) ∈ (0[,)+∞))
2925, 28sselid 3972 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (π»β€˜(π‘›β€˜0)) ∈ ℝ)
3024, 29remulcld 11241 . . . 4 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ ((Ξ›β€˜(π‘›β€˜0)) Β· (π»β€˜(π‘›β€˜0))) ∈ ℝ)
31 1ex 11207 . . . . . . . . . . 11 1 ∈ V
3231tpid2 4766 . . . . . . . . . 10 1 ∈ {0, 1, 2}
3332, 20eleqtrri 2824 . . . . . . . . 9 1 ∈ (0..^3)
3433a1i 11 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 1 ∈ (0..^3))
3517, 34ffvelcdmd 7077 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (π‘›β€˜1) ∈ β„•)
3610, 35ffvelcdmd 7077 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (Ξ›β€˜(π‘›β€˜1)) ∈ ℝ)
37 hgt750leme.k . . . . . . . . 9 (πœ‘ β†’ 𝐾:β„•βŸΆ(0[,)+∞))
3837adantr 480 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 𝐾:β„•βŸΆ(0[,)+∞))
3938, 35ffvelcdmd 7077 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (πΎβ€˜(π‘›β€˜1)) ∈ (0[,)+∞))
4025, 39sselid 3972 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (πΎβ€˜(π‘›β€˜1)) ∈ ℝ)
4136, 40remulcld 11241 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ ((Ξ›β€˜(π‘›β€˜1)) Β· (πΎβ€˜(π‘›β€˜1))) ∈ ℝ)
42 2ex 12286 . . . . . . . . . . 11 2 ∈ V
4342tpid3 4769 . . . . . . . . . 10 2 ∈ {0, 1, 2}
4443, 20eleqtrri 2824 . . . . . . . . 9 2 ∈ (0..^3)
4544a1i 11 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 2 ∈ (0..^3))
4617, 45ffvelcdmd 7077 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (π‘›β€˜2) ∈ β„•)
4710, 46ffvelcdmd 7077 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (Ξ›β€˜(π‘›β€˜2)) ∈ ℝ)
4838, 46ffvelcdmd 7077 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (πΎβ€˜(π‘›β€˜2)) ∈ (0[,)+∞))
4925, 48sselid 3972 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (πΎβ€˜(π‘›β€˜2)) ∈ ℝ)
5047, 49remulcld 11241 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ ((Ξ›β€˜(π‘›β€˜2)) Β· (πΎβ€˜(π‘›β€˜2))) ∈ ℝ)
5141, 50remulcld 11241 . . . 4 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (((Ξ›β€˜(π‘›β€˜1)) Β· (πΎβ€˜(π‘›β€˜1))) Β· ((Ξ›β€˜(π‘›β€˜2)) Β· (πΎβ€˜(π‘›β€˜2)))) ∈ ℝ)
5230, 51remulcld 11241 . . 3 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (((Ξ›β€˜(π‘›β€˜0)) Β· (π»β€˜(π‘›β€˜0))) Β· (((Ξ›β€˜(π‘›β€˜1)) Β· (πΎβ€˜(π‘›β€˜1))) Β· ((Ξ›β€˜(π‘›β€˜2)) Β· (πΎβ€˜(π‘›β€˜2))))) ∈ ℝ)
538, 52fsumrecl 15677 . 2 (πœ‘ β†’ Σ𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))(((Ξ›β€˜(π‘›β€˜0)) Β· (π»β€˜(π‘›β€˜0))) Β· (((Ξ›β€˜(π‘›β€˜1)) Β· (πΎβ€˜(π‘›β€˜1))) Β· ((Ξ›β€˜(π‘›β€˜2)) Β· (πΎβ€˜(π‘›β€˜2))))) ∈ ℝ)
54 3re 12289 . . . 4 3 ∈ ℝ
5554a1i 11 . . 3 (πœ‘ β†’ 3 ∈ ℝ)
56 1nn0 12485 . . . . . . . . 9 1 ∈ β„•0
57 0nn0 12484 . . . . . . . . . 10 0 ∈ β„•0
58 7nn0 12491 . . . . . . . . . . 11 7 ∈ β„•0
59 9nn0 12493 . . . . . . . . . . . 12 9 ∈ β„•0
60 5nn0 12489 . . . . . . . . . . . . . 14 5 ∈ β„•0
61 5nn 12295 . . . . . . . . . . . . . . 15 5 ∈ β„•
62 nnrp 12982 . . . . . . . . . . . . . . 15 (5 ∈ β„• β†’ 5 ∈ ℝ+)
6361, 62ax-mp 5 . . . . . . . . . . . . . 14 5 ∈ ℝ+
6460, 63rpdp2cl 32515 . . . . . . . . . . . . 13 55 ∈ ℝ+
6559, 64rpdp2cl 32515 . . . . . . . . . . . 12 955 ∈ ℝ+
6659, 65rpdp2cl 32515 . . . . . . . . . . 11 9955 ∈ ℝ+
6758, 66rpdp2cl 32515 . . . . . . . . . 10 79955 ∈ ℝ+
6857, 67rpdp2cl 32515 . . . . . . . . 9 079955 ∈ ℝ+
6956, 68rpdpcl 32536 . . . . . . . 8 (1.079955) ∈ ℝ+
7069a1i 11 . . . . . . 7 (πœ‘ β†’ (1.079955) ∈ ℝ+)
7170rpred 13013 . . . . . 6 (πœ‘ β†’ (1.079955) ∈ ℝ)
7271resqcld 14087 . . . . 5 (πœ‘ β†’ ((1.079955)↑2) ∈ ℝ)
73 4nn0 12488 . . . . . . . . 9 4 ∈ β„•0
74 4nn 12292 . . . . . . . . . . 11 4 ∈ β„•
75 nnrp 12982 . . . . . . . . . . 11 (4 ∈ β„• β†’ 4 ∈ ℝ+)
7674, 75ax-mp 5 . . . . . . . . . 10 4 ∈ ℝ+
7756, 76rpdp2cl 32515 . . . . . . . . 9 14 ∈ ℝ+
7873, 77rpdp2cl 32515 . . . . . . . 8 414 ∈ ℝ+
7956, 78rpdpcl 32536 . . . . . . 7 (1.414) ∈ ℝ+
8079a1i 11 . . . . . 6 (πœ‘ β†’ (1.414) ∈ ℝ+)
8180rpred 13013 . . . . 5 (πœ‘ β†’ (1.414) ∈ ℝ)
8272, 81remulcld 11241 . . . 4 (πœ‘ β†’ (((1.079955)↑2) Β· (1.414)) ∈ ℝ)
83 fveq1 6880 . . . . . . . . . 10 (𝑑 = 𝑐 β†’ (π‘‘β€˜0) = (π‘β€˜0))
8483eleq1d 2810 . . . . . . . . 9 (𝑑 = 𝑐 β†’ ((π‘‘β€˜0) ∈ (𝑂 ∩ β„™) ↔ (π‘β€˜0) ∈ (𝑂 ∩ β„™)))
8584notbid 318 . . . . . . . 8 (𝑑 = 𝑐 β†’ (Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™) ↔ Β¬ (π‘β€˜0) ∈ (𝑂 ∩ β„™)))
8685cbvrabv 3434 . . . . . . 7 {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} = {𝑐 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘β€˜0) ∈ (𝑂 ∩ β„™)}
8786ssrab3 4072 . . . . . 6 {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} βŠ† (β„•(reprβ€˜3)𝑁)
88 ssfi 9169 . . . . . 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 3997 . . . . . . . . 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 3974 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ 𝑛 ∈ (β„•(reprβ€˜3)𝑁))
9691, 92, 93, 95reprf 34113 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ 𝑛:(0..^3)βŸΆβ„•)
9721a1i 11 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ 0 ∈ (0..^3))
9896, 97ffvelcdmd 7077 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ (π‘›β€˜0) ∈ β„•)
9990, 98ffvelcdmd 7077 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ (Ξ›β€˜(π‘›β€˜0)) ∈ ℝ)
10033a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ 1 ∈ (0..^3))
10196, 100ffvelcdmd 7077 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ (π‘›β€˜1) ∈ β„•)
10290, 101ffvelcdmd 7077 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ (Ξ›β€˜(π‘›β€˜1)) ∈ ℝ)
10344a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ 2 ∈ (0..^3))
10496, 103ffvelcdmd 7077 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ (π‘›β€˜2) ∈ β„•)
10590, 104ffvelcdmd 7077 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ (Ξ›β€˜(π‘›β€˜2)) ∈ ℝ)
106102, 105remulcld 11241 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2))) ∈ ℝ)
10799, 106remulcld 11241 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))) ∈ ℝ)
10889, 107fsumrecl 15677 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))) ∈ ℝ)
10982, 108remulcld 11241 . . 3 (πœ‘ β†’ ((((1.079955)↑2) Β· (1.414)) Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2))))) ∈ ℝ)
11055, 109remulcld 11241 . 2 (πœ‘ β†’ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))))) ∈ ℝ)
111 4re 12293 . . . . . . . . . 10 4 ∈ ℝ
112 8re 12305 . . . . . . . . . 10 8 ∈ ℝ
113111, 112pm3.2i 470 . . . . . . . . 9 (4 ∈ ℝ ∧ 8 ∈ ℝ)
114 dp2cl 32513 . . . . . . . . 9 ((4 ∈ ℝ ∧ 8 ∈ ℝ) β†’ 48 ∈ ℝ)
115113, 114ax-mp 5 . . . . . . . 8 48 ∈ ℝ
11654, 115pm3.2i 470 . . . . . . 7 (3 ∈ ℝ ∧ 48 ∈ ℝ)
117 dp2cl 32513 . . . . . . 7 ((3 ∈ ℝ ∧ 48 ∈ ℝ) β†’ 348 ∈ ℝ)
118116, 117ax-mp 5 . . . . . 6 348 ∈ ℝ
119 dpcl 32524 . . . . . 6 ((7 ∈ β„•0 ∧ 348 ∈ ℝ) β†’ (7.348) ∈ ℝ)
12058, 118, 119mp2an 689 . . . . 5 (7.348) ∈ ℝ
121120a1i 11 . . . 4 (πœ‘ β†’ (7.348) ∈ ℝ)
1221nnrpd 13011 . . . . . 6 (πœ‘ β†’ 𝑁 ∈ ℝ+)
123122relogcld 26473 . . . . 5 (πœ‘ β†’ (logβ€˜π‘) ∈ ℝ)
1241nnred 12224 . . . . . 6 (πœ‘ β†’ 𝑁 ∈ ℝ)
125122rpge0d 13017 . . . . . 6 (πœ‘ β†’ 0 ≀ 𝑁)
126124, 125resqrtcld 15361 . . . . 5 (πœ‘ β†’ (βˆšβ€˜π‘) ∈ ℝ)
127122rpsqrtcld 15355 . . . . . 6 (πœ‘ β†’ (βˆšβ€˜π‘) ∈ ℝ+)
128127rpne0d 13018 . . . . 5 (πœ‘ β†’ (βˆšβ€˜π‘) β‰  0)
129123, 126, 128redivcld 12039 . . . 4 (πœ‘ β†’ ((logβ€˜π‘) / (βˆšβ€˜π‘)) ∈ ℝ)
130121, 129remulcld 11241 . . 3 (πœ‘ β†’ ((7.348) Β· ((logβ€˜π‘) / (βˆšβ€˜π‘))) ∈ ℝ)
131124resqcld 14087 . . 3 (πœ‘ β†’ (𝑁↑2) ∈ ℝ)
132130, 131remulcld 11241 . 2 (πœ‘ β†’ (((7.348) Β· ((logβ€˜π‘) / (βˆšβ€˜π‘))) Β· (𝑁↑2)) ∈ ℝ)
133 0re 11213 . . . . . . . . . . 11 0 ∈ ℝ
134 7re 12302 . . . . . . . . . . . . 13 7 ∈ ℝ
135 9re 12308 . . . . . . . . . . . . . . 15 9 ∈ ℝ
136 5re 12296 . . . . . . . . . . . . . . . . . . 19 5 ∈ ℝ
137136, 136pm3.2i 470 . . . . . . . . . . . . . . . . . 18 (5 ∈ ℝ ∧ 5 ∈ ℝ)
138 dp2cl 32513 . . . . . . . . . . . . . . . . . 18 ((5 ∈ ℝ ∧ 5 ∈ ℝ) β†’ 55 ∈ ℝ)
139137, 138ax-mp 5 . . . . . . . . . . . . . . . . 17 55 ∈ ℝ
140135, 139pm3.2i 470 . . . . . . . . . . . . . . . 16 (9 ∈ ℝ ∧ 55 ∈ ℝ)
141 dp2cl 32513 . . . . . . . . . . . . . . . 16 ((9 ∈ ℝ ∧ 55 ∈ ℝ) β†’ 955 ∈ ℝ)
142140, 141ax-mp 5 . . . . . . . . . . . . . . 15 955 ∈ ℝ
143135, 142pm3.2i 470 . . . . . . . . . . . . . 14 (9 ∈ ℝ ∧ 955 ∈ ℝ)
144 dp2cl 32513 . . . . . . . . . . . . . 14 ((9 ∈ ℝ ∧ 955 ∈ ℝ) β†’ 9955 ∈ ℝ)
145143, 144ax-mp 5 . . . . . . . . . . . . 13 9955 ∈ ℝ
146134, 145pm3.2i 470 . . . . . . . . . . . 12 (7 ∈ ℝ ∧ 9955 ∈ ℝ)
147 dp2cl 32513 . . . . . . . . . . . 12 ((7 ∈ ℝ ∧ 9955 ∈ ℝ) β†’ 79955 ∈ ℝ)
148146, 147ax-mp 5 . . . . . . . . . . 11 79955 ∈ ℝ
149133, 148pm3.2i 470 . . . . . . . . . 10 (0 ∈ ℝ ∧ 79955 ∈ ℝ)
150 dp2cl 32513 . . . . . . . . . 10 ((0 ∈ ℝ ∧ 79955 ∈ ℝ) β†’ 079955 ∈ ℝ)
151149, 150ax-mp 5 . . . . . . . . 9 079955 ∈ ℝ
152 dpcl 32524 . . . . . . . . 9 ((1 ∈ β„•0 ∧ 079955 ∈ ℝ) β†’ (1.079955) ∈ ℝ)
15356, 151, 152mp2an 689 . . . . . . . 8 (1.079955) ∈ ℝ
154153a1i 11 . . . . . . 7 (πœ‘ β†’ (1.079955) ∈ ℝ)
155154resqcld 14087 . . . . . 6 (πœ‘ β†’ ((1.079955)↑2) ∈ ℝ)
156 1re 11211 . . . . . . . . . . . 12 1 ∈ ℝ
157156, 111pm3.2i 470 . . . . . . . . . . 11 (1 ∈ ℝ ∧ 4 ∈ ℝ)
158 dp2cl 32513 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 4 ∈ ℝ) β†’ 14 ∈ ℝ)
159157, 158ax-mp 5 . . . . . . . . . 10 14 ∈ ℝ
160111, 159pm3.2i 470 . . . . . . . . 9 (4 ∈ ℝ ∧ 14 ∈ ℝ)
161 dp2cl 32513 . . . . . . . . 9 ((4 ∈ ℝ ∧ 14 ∈ ℝ) β†’ 414 ∈ ℝ)
162160, 161ax-mp 5 . . . . . . . 8 414 ∈ ℝ
163 dpcl 32524 . . . . . . . 8 ((1 ∈ β„•0 ∧ 414 ∈ ℝ) β†’ (1.414) ∈ ℝ)
16456, 162, 163mp2an 689 . . . . . . 7 (1.414) ∈ ℝ
165164a1i 11 . . . . . 6 (πœ‘ β†’ (1.414) ∈ ℝ)
166155, 165remulcld 11241 . . . . 5 (πœ‘ β†’ (((1.079955)↑2) Β· (1.414)) ∈ ℝ)
16736, 47remulcld 11241 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2))) ∈ ℝ)
16824, 167remulcld 11241 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))) ∈ ℝ)
1698, 168fsumrecl 15677 . . . . 5 (πœ‘ β†’ Σ𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))) ∈ ℝ)
170166, 169remulcld 11241 . . . 4 (πœ‘ β†’ ((((1.079955)↑2) Β· (1.414)) Β· Σ𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2))))) ∈ ℝ)
17155, 108remulcld 11241 . . . . 5 (πœ‘ β†’ (3 Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2))))) ∈ ℝ)
172166, 171remulcld 11241 . . . 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 34154 . . . 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 12283 . . . . . . . 8 2 ∈ ℝ
178177a1i 11 . . . . . . 7 (πœ‘ β†’ 2 ∈ ℝ)
179 10nn0 12692 . . . . . . . . . 10 10 ∈ β„•0
180 2nn0 12486 . . . . . . . . . . 11 2 ∈ β„•0
181180, 58deccl 12689 . . . . . . . . . 10 27 ∈ β„•0
182179, 181nn0expcli 14051 . . . . . . . . 9 (10↑27) ∈ β„•0
183182nn0rei 12480 . . . . . . . 8 (10↑27) ∈ ℝ
184183a1i 11 . . . . . . 7 (πœ‘ β†’ (10↑27) ∈ ℝ)
185179numexp1 17009 . . . . . . . . . 10 (10↑1) = 10
186179nn0rei 12480 . . . . . . . . . 10 10 ∈ ℝ
187185, 186eqeltri 2821 . . . . . . . . 9 (10↑1) ∈ ℝ
188187a1i 11 . . . . . . . 8 (πœ‘ β†’ (10↑1) ∈ ℝ)
189 1nn 12220 . . . . . . . . . . 11 1 ∈ β„•
190 2lt9 12414 . . . . . . . . . . . 12 2 < 9
191177, 135, 190ltleii 11334 . . . . . . . . . . 11 2 ≀ 9
192189, 57, 180, 191declei 12710 . . . . . . . . . 10 2 ≀ 10
193192, 185breqtrri 5165 . . . . . . . . 9 2 ≀ (10↑1)
194193a1i 11 . . . . . . . 8 (πœ‘ β†’ 2 ≀ (10↑1))
195 1z 12589 . . . . . . . . . . . 12 1 ∈ β„€
196181nn0zi 12584 . . . . . . . . . . . 12 27 ∈ β„€
197186, 195, 1963pm3.2i 1336 . . . . . . . . . . 11 (10 ∈ ℝ ∧ 1 ∈ β„€ ∧ 27 ∈ β„€)
198 1lt10 12813 . . . . . . . . . . 11 1 < 10
199197, 198pm3.2i 470 . . . . . . . . . 10 ((10 ∈ ℝ ∧ 1 ∈ β„€ ∧ 27 ∈ β„€) ∧ 1 < 10)
200 2nn 12282 . . . . . . . . . . 11 2 ∈ β„•
201 1lt9 12415 . . . . . . . . . . . 12 1 < 9
202156, 135, 201ltleii 11334 . . . . . . . . . . 11 1 ≀ 9
203200, 58, 56, 202declei 12710 . . . . . . . . . 10 1 ≀ 27
204 leexp2 14133 . . . . . . . . . . 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 11368 . . . . . . 7 (πœ‘ β†’ 2 ≀ (10↑27))
209 hgt750leme.0 . . . . . . 7 (πœ‘ β†’ (10↑27) ≀ 𝑁)
210178, 184, 124, 208, 209letrd 11368 . . . . . 6 (πœ‘ β†’ 2 ≀ 𝑁)
211 eqid 2724 . . . . . 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 34158 . . . . 5 (πœ‘ β†’ Σ𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))) ≀ (3 Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2))))))
213 2z 12591 . . . . . . . . 9 2 ∈ β„€
214213a1i 11 . . . . . . . 8 (πœ‘ β†’ 2 ∈ β„€)
21570, 214rpexpcld 14207 . . . . . . 7 (πœ‘ β†’ ((1.079955)↑2) ∈ ℝ+)
216215, 80rpmulcld 13029 . . . . . 6 (πœ‘ β†’ (((1.079955)↑2) Β· (1.414)) ∈ ℝ+)
217169, 171, 216lemul2d 13057 . . . . 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 11368 . . 3 (πœ‘ β†’ Σ𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))(((Ξ›β€˜(π‘›β€˜0)) Β· (π»β€˜(π‘›β€˜0))) Β· (((Ξ›β€˜(π‘›β€˜1)) Β· (πΎβ€˜(π‘›β€˜1))) Β· ((Ξ›β€˜(π‘›β€˜2)) Β· (πΎβ€˜(π‘›β€˜2))))) ≀ ((((1.079955)↑2) Β· (1.414)) Β· (3 Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))))))
220154recnd 11239 . . . . . 6 (πœ‘ β†’ (1.079955) ∈ β„‚)
221220sqcld 14106 . . . . 5 (πœ‘ β†’ ((1.079955)↑2) ∈ β„‚)
222165recnd 11239 . . . . 5 (πœ‘ β†’ (1.414) ∈ β„‚)
223221, 222mulcld 11231 . . . 4 (πœ‘ β†’ (((1.079955)↑2) Β· (1.414)) ∈ β„‚)
224 3cn 12290 . . . . 5 3 ∈ β„‚
225224a1i 11 . . . 4 (πœ‘ β†’ 3 ∈ β„‚)
226108recnd 11239 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))) ∈ β„‚)
227223, 225, 226mul12d 11420 . . 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 5164 . 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 13934 . . . . . . . . . . 11 (1...𝑁) ∈ Fin
230 diffi 9175 . . . . . . . . . . 11 ((1...𝑁) ∈ Fin β†’ ((1...𝑁) βˆ– β„™) ∈ Fin)
231229, 230ax-mp 5 . . . . . . . . . 10 ((1...𝑁) βˆ– β„™) ∈ Fin
232 snfi 9040 . . . . . . . . . 10 {2} ∈ Fin
233 unfi 9168 . . . . . . . . . 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 13529 . . . . . . . . . . . . 13 (1...𝑁) βŠ† β„•
238237a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ (1...𝑁) βŠ† β„•)
239238ssdifssd 4134 . . . . . . . . . . 11 (πœ‘ β†’ ((1...𝑁) βˆ– β„™) βŠ† β„•)
240200a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ 2 ∈ β„•)
241240snssd 4804 . . . . . . . . . . 11 (πœ‘ β†’ {2} βŠ† β„•)
242239, 241unssd 4178 . . . . . . . . . 10 (πœ‘ β†’ (((1...𝑁) βˆ– β„™) βˆͺ {2}) βŠ† β„•)
243242sselda 3974 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})) β†’ 𝑖 ∈ β„•)
244236, 243ffvelcdmd 7077 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})) β†’ (Ξ›β€˜π‘–) ∈ ℝ)
245235, 244fsumrecl 15677 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) ∈ ℝ)
246 chpvalz 34129 . . . . . . . . 9 (𝑁 ∈ β„€ β†’ (Οˆβ€˜π‘) = Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))
24712, 246syl 17 . . . . . . . 8 (πœ‘ β†’ (Οˆβ€˜π‘) = Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))
248 chpf 26971 . . . . . . . . . 10 ψ:β„βŸΆβ„
249248a1i 11 . . . . . . . . 9 (πœ‘ β†’ ψ:β„βŸΆβ„)
250249, 124ffvelcdmd 7077 . . . . . . . 8 (πœ‘ β†’ (Οˆβ€˜π‘) ∈ ℝ)
251247, 250eqeltrrd 2826 . . . . . . 7 (πœ‘ β†’ Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—) ∈ ℝ)
252245, 251remulcld 11241 . . . . . 6 (πœ‘ β†’ (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—)) ∈ ℝ)
253123, 252remulcld 11241 . . . . 5 (πœ‘ β†’ ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))) ∈ ℝ)
25482, 253remulcld 11241 . . . 4 (πœ‘ β†’ ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—)))) ∈ ℝ)
25555, 254remulcld 11241 . . 3 (πœ‘ β†’ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))))) ∈ ℝ)
256176, 1, 210, 86hgt750lemb 34157 . . . . 5 (πœ‘ β†’ Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))) ≀ ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))))
257108, 253, 216lemul2d 13057 . . . . 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 12977 . . . . . 6 3 ∈ ℝ+
260259a1i 11 . . . . 5 (πœ‘ β†’ 3 ∈ ℝ+)
261109, 254, 260lemul2d 13057 . . . 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 12299 . . . . . . . . . . . . . . . . 17 6 ∈ ℝ
264263, 54pm3.2i 470 . . . . . . . . . . . . . . . 16 (6 ∈ ℝ ∧ 3 ∈ ℝ)
265 dp2cl 32513 . . . . . . . . . . . . . . . 16 ((6 ∈ ℝ ∧ 3 ∈ ℝ) β†’ 63 ∈ ℝ)
266264, 265ax-mp 5 . . . . . . . . . . . . . . 15 63 ∈ ℝ
267177, 266pm3.2i 470 . . . . . . . . . . . . . 14 (2 ∈ ℝ ∧ 63 ∈ ℝ)
268 dp2cl 32513 . . . . . . . . . . . . . 14 ((2 ∈ ℝ ∧ 63 ∈ ℝ) β†’ 263 ∈ ℝ)
269267, 268ax-mp 5 . . . . . . . . . . . . 13 263 ∈ ℝ
270111, 269pm3.2i 470 . . . . . . . . . . . 12 (4 ∈ ℝ ∧ 263 ∈ ℝ)
271 dp2cl 32513 . . . . . . . . . . . 12 ((4 ∈ ℝ ∧ 263 ∈ ℝ) β†’ 4263 ∈ ℝ)
272270, 271ax-mp 5 . . . . . . . . . . 11 4263 ∈ ℝ
273 dpcl 32524 . . . . . . . . . . 11 ((1 ∈ β„•0 ∧ 4263 ∈ ℝ) β†’ (1.4263) ∈ ℝ)
27456, 272, 273mp2an 689 . . . . . . . . . 10 (1.4263) ∈ ℝ
275274a1i 11 . . . . . . . . 9 (πœ‘ β†’ (1.4263) ∈ ℝ)
276275, 126remulcld 11241 . . . . . . . 8 (πœ‘ β†’ ((1.4263) Β· (βˆšβ€˜π‘)) ∈ ℝ)
277112, 54pm3.2i 470 . . . . . . . . . . . . . . . . . 18 (8 ∈ ℝ ∧ 3 ∈ ℝ)
278 dp2cl 32513 . . . . . . . . . . . . . . . . . 18 ((8 ∈ ℝ ∧ 3 ∈ ℝ) β†’ 83 ∈ ℝ)
279277, 278ax-mp 5 . . . . . . . . . . . . . . . . 17 83 ∈ ℝ
280112, 279pm3.2i 470 . . . . . . . . . . . . . . . 16 (8 ∈ ℝ ∧ 83 ∈ ℝ)
281 dp2cl 32513 . . . . . . . . . . . . . . . 16 ((8 ∈ ℝ ∧ 83 ∈ ℝ) β†’ 883 ∈ ℝ)
282280, 281ax-mp 5 . . . . . . . . . . . . . . 15 883 ∈ ℝ
28354, 282pm3.2i 470 . . . . . . . . . . . . . 14 (3 ∈ ℝ ∧ 883 ∈ ℝ)
284 dp2cl 32513 . . . . . . . . . . . . . 14 ((3 ∈ ℝ ∧ 883 ∈ ℝ) β†’ 3883 ∈ ℝ)
285283, 284ax-mp 5 . . . . . . . . . . . . 13 3883 ∈ ℝ
286133, 285pm3.2i 470 . . . . . . . . . . . 12 (0 ∈ ℝ ∧ 3883 ∈ ℝ)
287 dp2cl 32513 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ 3883 ∈ ℝ) β†’ 03883 ∈ ℝ)
288286, 287ax-mp 5 . . . . . . . . . . 11 03883 ∈ ℝ
289 dpcl 32524 . . . . . . . . . . 11 ((1 ∈ β„•0 ∧ 03883 ∈ ℝ) β†’ (1.03883) ∈ ℝ)
29056, 288, 289mp2an 689 . . . . . . . . . 10 (1.03883) ∈ ℝ
291290a1i 11 . . . . . . . . 9 (πœ‘ β†’ (1.03883) ∈ ℝ)
292291, 124remulcld 11241 . . . . . . . 8 (πœ‘ β†’ ((1.03883) Β· 𝑁) ∈ ℝ)
293276, 292remulcld 11241 . . . . . . 7 (πœ‘ β†’ (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁)) ∈ ℝ)
294123, 293remulcld 11241 . . . . . 6 (πœ‘ β†’ ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))) ∈ ℝ)
29582, 294remulcld 11241 . . . . 5 (πœ‘ β†’ ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁)))) ∈ ℝ)
29655, 295remulcld 11241 . . . 4 (πœ‘ β†’ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))))) ∈ ℝ)
297 vmage0 26969 . . . . . . . . . . 11 (𝑖 ∈ β„• β†’ 0 ≀ (Ξ›β€˜π‘–))
298243, 297syl 17 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})) β†’ 0 ≀ (Ξ›β€˜π‘–))
299235, 244, 298fsumge0 15738 . . . . . . . . 9 (πœ‘ β†’ 0 ≀ Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–))
3001, 209hgt750lemd 34149 . . . . . . . . 9 (πœ‘ β†’ Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) < ((1.4263) Β· (βˆšβ€˜π‘)))
301 fzfid 13935 . . . . . . . . . 10 (πœ‘ β†’ (1...𝑁) ∈ Fin)
3029a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ (1...𝑁)) β†’ Ξ›:β„•βŸΆβ„)
303238sselda 3974 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ (1...𝑁)) β†’ 𝑗 ∈ β„•)
304302, 303ffvelcdmd 7077 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (1...𝑁)) β†’ (Ξ›β€˜π‘—) ∈ ℝ)
305 vmage0 26969 . . . . . . . . . . 11 (𝑗 ∈ β„• β†’ 0 ≀ (Ξ›β€˜π‘—))
306303, 305syl 17 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (1...𝑁)) β†’ 0 ≀ (Ξ›β€˜π‘—))
307301, 304, 306fsumge0 15738 . . . . . . . . 9 (πœ‘ β†’ 0 ≀ Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))
3081hgt750lemc 34148 . . . . . . . . 9 (πœ‘ β†’ Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—) < ((1.03883) Β· 𝑁))
309245, 276, 251, 292, 299, 300, 307, 308ltmul12ad 12152 . . . . . . . 8 (πœ‘ β†’ (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—)) < (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁)))
310252, 293, 309ltled 11359 . . . . . . 7 (πœ‘ β†’ (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—)) ≀ (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁)))
311156a1i 11 . . . . . . . . . 10 (πœ‘ β†’ 1 ∈ ℝ)
312 1lt2 12380 . . . . . . . . . . 11 1 < 2
313312a1i 11 . . . . . . . . . 10 (πœ‘ β†’ 1 < 2)
314311, 178, 124, 313, 210ltletrd 11371 . . . . . . . . 9 (πœ‘ β†’ 1 < 𝑁)
315124, 314rplogcld 26479 . . . . . . . 8 (πœ‘ β†’ (logβ€˜π‘) ∈ ℝ+)
316252, 293, 315lemul2d 13057 . . . . . . 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 13057 . . . . . 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 13057 . . . . 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 14147 . . . . . . . . . 10 ((1.079955)↑2) ∈ ℝ
323322, 164remulcli 11227 . . . . . . . . 9 (((1.079955)↑2) Β· (1.414)) ∈ ℝ
324274, 290remulcli 11227 . . . . . . . . 9 ((1.4263) Β· (1.03883)) ∈ ℝ
325323, 324remulcli 11227 . . . . . . . 8 ((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883))) ∈ ℝ
32654, 325remulcli 11227 . . . . . . 7 (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883)))) ∈ ℝ
327 hgt750lem2 34153 . . . . . . 7 (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883)))) < (7.348)
328326, 120, 327ltleii 11334 . . . . . 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 13030 . . . . . . . 8 (πœ‘ β†’ ((logβ€˜π‘) / (βˆšβ€˜π‘)) ∈ ℝ+)
331122, 214rpexpcld 14207 . . . . . . . 8 (πœ‘ β†’ (𝑁↑2) ∈ ℝ+)
332330, 331rpmulcld 13029 . . . . . . 7 (πœ‘ β†’ (((logβ€˜π‘) / (βˆšβ€˜π‘)) Β· (𝑁↑2)) ∈ ℝ+)
333329, 121, 332lemul1d 13056 . . . . . 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 11239 . . . . . . . . . . . . . 14 (πœ‘ β†’ (1.4263) ∈ β„‚)
336126recnd 11239 . . . . . . . . . . . . . 14 (πœ‘ β†’ (βˆšβ€˜π‘) ∈ β„‚)
337291recnd 11239 . . . . . . . . . . . . . 14 (πœ‘ β†’ (1.03883) ∈ β„‚)
338124recnd 11239 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑁 ∈ β„‚)
339335, 336, 337, 338mul4d 11423 . . . . . . . . . . . . 13 (πœ‘ β†’ (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁)) = (((1.4263) Β· (1.03883)) Β· ((βˆšβ€˜π‘) Β· 𝑁)))
340339oveq2d 7417 . . . . . . . . . . . 12 (πœ‘ β†’ ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))) = ((logβ€˜π‘) Β· (((1.4263) Β· (1.03883)) Β· ((βˆšβ€˜π‘) Β· 𝑁))))
341123recnd 11239 . . . . . . . . . . . . 13 (πœ‘ β†’ (logβ€˜π‘) ∈ β„‚)
342335, 337mulcld 11231 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((1.4263) Β· (1.03883)) ∈ β„‚)
343336, 338mulcld 11231 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((βˆšβ€˜π‘) Β· 𝑁) ∈ β„‚)
344342, 343mulcld 11231 . . . . . . . . . . . . 13 (πœ‘ β†’ (((1.4263) Β· (1.03883)) Β· ((βˆšβ€˜π‘) Β· 𝑁)) ∈ β„‚)
345341, 344mulcomd 11232 . . . . . . . . . . . 12 (πœ‘ β†’ ((logβ€˜π‘) Β· (((1.4263) Β· (1.03883)) Β· ((βˆšβ€˜π‘) Β· 𝑁))) = ((((1.4263) Β· (1.03883)) Β· ((βˆšβ€˜π‘) Β· 𝑁)) Β· (logβ€˜π‘)))
346340, 345eqtrd 2764 . . . . . . . . . . 11 (πœ‘ β†’ ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))) = ((((1.4263) Β· (1.03883)) Β· ((βˆšβ€˜π‘) Β· 𝑁)) Β· (logβ€˜π‘)))
347342, 343, 341mulassd 11234 . . . . . . . . . . 11 (πœ‘ β†’ ((((1.4263) Β· (1.03883)) Β· ((βˆšβ€˜π‘) Β· 𝑁)) Β· (logβ€˜π‘)) = (((1.4263) Β· (1.03883)) Β· (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘))))
348346, 347eqtrd 2764 . . . . . . . . . 10 (πœ‘ β†’ ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))) = (((1.4263) Β· (1.03883)) Β· (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘))))
349348oveq2d 7417 . . . . . . . . 9 (πœ‘ β†’ ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁)))) = ((((1.079955)↑2) Β· (1.414)) Β· (((1.4263) Β· (1.03883)) Β· (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘)))))
35082recnd 11239 . . . . . . . . . 10 (πœ‘ β†’ (((1.079955)↑2) Β· (1.414)) ∈ β„‚)
351343, 341mulcld 11231 . . . . . . . . . 10 (πœ‘ β†’ (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘)) ∈ β„‚)
352350, 342, 351mulassd 11234 . . . . . . . . 9 (πœ‘ β†’ (((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883))) Β· (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘))) = ((((1.079955)↑2) Β· (1.414)) Β· (((1.4263) Β· (1.03883)) Β· (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘)))))
353349, 352eqtr4d 2767 . . . . . . . 8 (πœ‘ β†’ ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁)))) = (((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883))) Β· (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘))))
354353oveq2d 7417 . . . . . . 7 (πœ‘ β†’ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))))) = (3 Β· (((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883))) Β· (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘)))))
35555recnd 11239 . . . . . . . 8 (πœ‘ β†’ 3 ∈ β„‚)
356350, 342mulcld 11231 . . . . . . . 8 (πœ‘ β†’ ((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883))) ∈ β„‚)
357355, 356, 351mulassd 11234 . . . . . . 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 2767 . . . . . 6 (πœ‘ β†’ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))))) = ((3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883)))) Β· (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘))))
359131recnd 11239 . . . . . . . . 9 (πœ‘ β†’ (𝑁↑2) ∈ β„‚)
360341, 336, 359, 128div32d 12010 . . . . . . . 8 (πœ‘ β†’ (((logβ€˜π‘) / (βˆšβ€˜π‘)) Β· (𝑁↑2)) = ((logβ€˜π‘) Β· ((𝑁↑2) / (βˆšβ€˜π‘))))
361359, 336, 128divcld 11987 . . . . . . . . 9 (πœ‘ β†’ ((𝑁↑2) / (βˆšβ€˜π‘)) ∈ β„‚)
362341, 361mulcomd 11232 . . . . . . . 8 (πœ‘ β†’ ((logβ€˜π‘) Β· ((𝑁↑2) / (βˆšβ€˜π‘))) = (((𝑁↑2) / (βˆšβ€˜π‘)) Β· (logβ€˜π‘)))
363338sqvald 14105 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑁↑2) = (𝑁 Β· 𝑁))
364363oveq1d 7416 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑁↑2) / (βˆšβ€˜π‘)) = ((𝑁 Β· 𝑁) / (βˆšβ€˜π‘)))
365338, 338, 336, 128divassd 12022 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑁 Β· 𝑁) / (βˆšβ€˜π‘)) = (𝑁 Β· (𝑁 / (βˆšβ€˜π‘))))
366 divsqrtid 34095 . . . . . . . . . . . . 13 (𝑁 ∈ ℝ+ β†’ (𝑁 / (βˆšβ€˜π‘)) = (βˆšβ€˜π‘))
367122, 366syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑁 / (βˆšβ€˜π‘)) = (βˆšβ€˜π‘))
368367oveq2d 7417 . . . . . . . . . . 11 (πœ‘ β†’ (𝑁 Β· (𝑁 / (βˆšβ€˜π‘))) = (𝑁 Β· (βˆšβ€˜π‘)))
369364, 365, 3683eqtrd 2768 . . . . . . . . . 10 (πœ‘ β†’ ((𝑁↑2) / (βˆšβ€˜π‘)) = (𝑁 Β· (βˆšβ€˜π‘)))
370338, 336mulcomd 11232 . . . . . . . . . 10 (πœ‘ β†’ (𝑁 Β· (βˆšβ€˜π‘)) = ((βˆšβ€˜π‘) Β· 𝑁))
371369, 370eqtrd 2764 . . . . . . . . 9 (πœ‘ β†’ ((𝑁↑2) / (βˆšβ€˜π‘)) = ((βˆšβ€˜π‘) Β· 𝑁))
372371oveq1d 7416 . . . . . . . 8 (πœ‘ β†’ (((𝑁↑2) / (βˆšβ€˜π‘)) Β· (logβ€˜π‘)) = (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘)))
373360, 362, 3723eqtrrd 2769 . . . . . . 7 (πœ‘ β†’ (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘)) = (((logβ€˜π‘) / (βˆšβ€˜π‘)) Β· (𝑁↑2)))
374373oveq2d 7417 . . . . . 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 2764 . . . . 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 11239 . . . . . 6 (πœ‘ β†’ (7.348) ∈ β„‚)
377129recnd 11239 . . . . . 6 (πœ‘ β†’ ((logβ€˜π‘) / (βˆšβ€˜π‘)) ∈ β„‚)
378376, 377, 359mulassd 11234 . . . . 5 (πœ‘ β†’ (((7.348) Β· ((logβ€˜π‘) / (βˆšβ€˜π‘))) Β· (𝑁↑2)) = ((7.348) Β· (((logβ€˜π‘) / (βˆšβ€˜π‘)) Β· (𝑁↑2))))
379334, 375, 3783brtr4d 5170 . . . 4 (πœ‘ β†’ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))))) ≀ (((7.348) Β· ((logβ€˜π‘) / (βˆšβ€˜π‘))) Β· (𝑁↑2)))
380255, 296, 132, 321, 379letrd 11368 . . 3 (πœ‘ β†’ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) Β· Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))))) ≀ (((7.348) Β· ((logβ€˜π‘) / (βˆšβ€˜π‘))) Β· (𝑁↑2)))
381110, 255, 132, 262, 380letrd 11368 . 2 (πœ‘ β†’ (3 Β· ((((1.079955)↑2) Β· (1.414)) Β· Σ𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ((Ξ›β€˜(π‘›β€˜0)) Β· ((Ξ›β€˜(π‘›β€˜1)) Β· (Ξ›β€˜(π‘›β€˜2)))))) ≀ (((7.348) Β· ((logβ€˜π‘) / (βˆšβ€˜π‘))) Β· (𝑁↑2)))
38253, 110, 132, 228, 381letrd 11368 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 1084   = wceq 1533   ∈ wcel 2098  {crab 3424   βˆ– cdif 3937   βˆͺ cun 3938   ∩ cin 3939   βŠ† wss 3940  ifcif 4520  {csn 4620  {cpr 4622  {ctp 4624   class class class wbr 5138   ↦ cmpt 5221   I cid 5563   β†Ύ cres 5668   ∘ ccom 5670  βŸΆwf 6529  β€˜cfv 6533  (class class class)co 7401  Fincfn 8935  β„‚cc 11104  β„cr 11105  0cc0 11106  1c1 11107   Β· cmul 11111  +∞cpnf 11242   < clt 11245   ≀ cle 11246   / cdiv 11868  β„•cn 12209  2c2 12264  3c3 12265  4c4 12266  5c5 12267  6c6 12268  7c7 12269  8c8 12270  9c9 12271  β„•0cn0 12469  β„€cz 12555  cdc 12674  β„+crp 12971  [,)cico 13323  ...cfz 13481  ..^cfzo 13624  β†‘cexp 14024  βˆšcsqrt 15177  Ξ£csu 15629   βˆ₯ cdvds 16194  β„™cprime 16605  pmTrspcpmtr 19351  logclog 26405  Ξ›cvma 26940  Οˆcchp 26941  cdp2 32504  .cdp 32521  reprcrepr 34109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-reg 9583  ax-inf2 9632  ax-ac2 10454  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185  ax-ros335 34146  ax-ros336 34147
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-supp 8141  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-oadd 8465  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-r1 9755  df-rank 9756  df-dju 9892  df-card 9930  df-ac 10107  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-xnn0 12542  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ioc 13326  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-mod 13832  df-seq 13964  df-exp 14025  df-fac 14231  df-bc 14260  df-hash 14288  df-shft 15011  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-limsup 15412  df-clim 15429  df-rlim 15430  df-sum 15630  df-prod 15847  df-ef 16008  df-sin 16010  df-cos 16011  df-tan 16012  df-pi 16013  df-dvds 16195  df-gcd 16433  df-prm 16606  df-pc 16769  df-struct 17079  df-sets 17096  df-slot 17114  df-ndx 17126  df-base 17144  df-ress 17173  df-plusg 17209  df-mulr 17210  df-starv 17211  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-hom 17220  df-cco 17221  df-rest 17367  df-topn 17368  df-0g 17386  df-gsum 17387  df-topgen 17388  df-pt 17389  df-prds 17392  df-xrs 17447  df-qtop 17452  df-imas 17453  df-xps 17455  df-mre 17529  df-mrc 17530  df-acs 17532  df-mgm 18563  df-sgrp 18642  df-mnd 18658  df-submnd 18704  df-mulg 18986  df-cntz 19223  df-pmtr 19352  df-cmn 19692  df-psmet 21220  df-xmet 21221  df-met 21222  df-bl 21223  df-mopn 21224  df-fbas 21225  df-fg 21226  df-cnfld 21229  df-top 22718  df-topon 22735  df-topsp 22757  df-bases 22771  df-cld 22845  df-ntr 22846  df-cls 22847  df-nei 22924  df-lp 22962  df-perf 22963  df-cn 23053  df-cnp 23054  df-haus 23141  df-cmp 23213  df-tx 23388  df-hmeo 23581  df-fil 23672  df-fm 23764  df-flim 23765  df-flf 23766  df-xms 24148  df-ms 24149  df-tms 24150  df-cncf 24720  df-limc 25717  df-dv 25718  df-ulm 26230  df-log 26407  df-atan 26715  df-cht 26945  df-vma 26946  df-chp 26947  df-dp2 32505  df-dp 32522  df-repr 34110
This theorem is referenced by:  tgoldbachgtde  34161
  Copyright terms: Public domain W3C validator