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 33659
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 4005 . . . . 5 (πœ‘ β†’ β„• βŠ† β„•)
62, 4, 5reprfi2 33624 . . . 4 (πœ‘ β†’ (β„•(reprβ€˜3)𝑁) ∈ Fin)
7 diffi 9176 . . . 4 ((β„•(reprβ€˜3)𝑁) ∈ Fin β†’ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁)) ∈ Fin)
86, 7syl 17 . . 3 (πœ‘ β†’ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁)) ∈ Fin)
9 vmaf 26613 . . . . . . 7 Ξ›:β„•βŸΆβ„
109a1i 11 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ Ξ›:β„•βŸΆβ„)
11 ssidd 4005 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ β„• βŠ† β„•)
121nnzd 12582 . . . . . . . . 9 (πœ‘ β†’ 𝑁 ∈ β„€)
1312adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 𝑁 ∈ β„€)
143a1i 11 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 3 ∈ β„•0)
15 simpr 486 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁)))
1615eldifad 3960 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 𝑛 ∈ (β„•(reprβ€˜3)𝑁))
1711, 13, 14, 16reprf 33613 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 𝑛:(0..^3)βŸΆβ„•)
18 c0ex 11205 . . . . . . . . . 10 0 ∈ V
1918tpid1 4772 . . . . . . . . 9 0 ∈ {0, 1, 2}
20 fzo0to3tp 13715 . . . . . . . . 9 (0..^3) = {0, 1, 2}
2119, 20eleqtrri 2833 . . . . . . . 8 0 ∈ (0..^3)
2221a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 0 ∈ (0..^3))
2317, 22ffvelcdmd 7085 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (π‘›β€˜0) ∈ β„•)
2410, 23ffvelcdmd 7085 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (Ξ›β€˜(π‘›β€˜0)) ∈ ℝ)
25 rge0ssre 13430 . . . . . 6 (0[,)+∞) βŠ† ℝ
26 hgt750leme.h . . . . . . . 8 (πœ‘ β†’ 𝐻:β„•βŸΆ(0[,)+∞))
2726adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 𝐻:β„•βŸΆ(0[,)+∞))
2827, 23ffvelcdmd 7085 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (π»β€˜(π‘›β€˜0)) ∈ (0[,)+∞))
2925, 28sselid 3980 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (π»β€˜(π‘›β€˜0)) ∈ ℝ)
3024, 29remulcld 11241 . . . 4 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ ((Ξ›β€˜(π‘›β€˜0)) Β· (π»β€˜(π‘›β€˜0))) ∈ ℝ)
31 1ex 11207 . . . . . . . . . . 11 1 ∈ V
3231tpid2 4774 . . . . . . . . . 10 1 ∈ {0, 1, 2}
3332, 20eleqtrri 2833 . . . . . . . . 9 1 ∈ (0..^3)
3433a1i 11 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 1 ∈ (0..^3))
3517, 34ffvelcdmd 7085 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (π‘›β€˜1) ∈ β„•)
3610, 35ffvelcdmd 7085 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (Ξ›β€˜(π‘›β€˜1)) ∈ ℝ)
37 hgt750leme.k . . . . . . . . 9 (πœ‘ β†’ 𝐾:β„•βŸΆ(0[,)+∞))
3837adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 𝐾:β„•βŸΆ(0[,)+∞))
3938, 35ffvelcdmd 7085 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (πΎβ€˜(π‘›β€˜1)) ∈ (0[,)+∞))
4025, 39sselid 3980 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (πΎβ€˜(π‘›β€˜1)) ∈ ℝ)
4136, 40remulcld 11241 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ ((Ξ›β€˜(π‘›β€˜1)) Β· (πΎβ€˜(π‘›β€˜1))) ∈ ℝ)
42 2ex 12286 . . . . . . . . . . 11 2 ∈ V
4342tpid3 4777 . . . . . . . . . 10 2 ∈ {0, 1, 2}
4443, 20eleqtrri 2833 . . . . . . . . 9 2 ∈ (0..^3)
4544a1i 11 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ 2 ∈ (0..^3))
4617, 45ffvelcdmd 7085 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (π‘›β€˜2) ∈ β„•)
4710, 46ffvelcdmd 7085 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (Ξ›β€˜(π‘›β€˜2)) ∈ ℝ)
4838, 46ffvelcdmd 7085 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ ((β„•(reprβ€˜3)𝑁) βˆ– ((𝑂 ∩ β„™)(reprβ€˜3)𝑁))) β†’ (πΎβ€˜(π‘›β€˜2)) ∈ (0[,)+∞))
4925, 48sselid 3980 . . . . . 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 32036 . . . . . . . . . . . . 13 55 ∈ ℝ+
6559, 64rpdp2cl 32036 . . . . . . . . . . . 12 955 ∈ ℝ+
6659, 65rpdp2cl 32036 . . . . . . . . . . 11 9955 ∈ ℝ+
6758, 66rpdp2cl 32036 . . . . . . . . . 10 79955 ∈ ℝ+
6857, 67rpdp2cl 32036 . . . . . . . . 9 079955 ∈ ℝ+
6956, 68rpdpcl 32057 . . . . . . . 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 32036 . . . . . . . . 9 14 ∈ ℝ+
7873, 77rpdp2cl 32036 . . . . . . . 8 414 ∈ ℝ+
7956, 78rpdpcl 32057 . . . . . . 7 (1.414) ∈ ℝ+
8079a1i 11 . . . . . 6 (πœ‘ β†’ (1.414) ∈ ℝ+)
8180rpred 13013 . . . . 5 (πœ‘ β†’ (1.414) ∈ ℝ)
8272, 81remulcld 11241 . . . 4 (πœ‘ β†’ (((1.079955)↑2) Β· (1.414)) ∈ ℝ)
83 fveq1 6888 . . . . . . . . . 10 (𝑑 = 𝑐 β†’ (π‘‘β€˜0) = (π‘β€˜0))
8483eleq1d 2819 . . . . . . . . 9 (𝑑 = 𝑐 β†’ ((π‘‘β€˜0) ∈ (𝑂 ∩ β„™) ↔ (π‘β€˜0) ∈ (𝑂 ∩ β„™)))
8584notbid 318 . . . . . . . 8 (𝑑 = 𝑐 β†’ (Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™) ↔ Β¬ (π‘β€˜0) ∈ (𝑂 ∩ β„™)))
8685cbvrabv 3443 . . . . . . 7 {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} = {𝑐 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘β€˜0) ∈ (𝑂 ∩ β„™)}
8786ssrab3 4080 . . . . . 6 {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} βŠ† (β„•(reprβ€˜3)𝑁)
88 ssfi 9170 . . . . . 6 (((β„•(reprβ€˜3)𝑁) ∈ Fin ∧ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} βŠ† (β„•(reprβ€˜3)𝑁)) β†’ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ∈ Fin)
896, 87, 88sylancl 587 . . . . 5 (πœ‘ β†’ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)} ∈ Fin)
909a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ Ξ›:β„•βŸΆβ„)
91 ssidd 4005 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ β„• βŠ† β„•)
9212adantr 482 . . . . . . . . 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 33613 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ 𝑛:(0..^3)βŸΆβ„•)
9721a1i 11 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ 0 ∈ (0..^3))
9896, 97ffvelcdmd 7085 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ (π‘›β€˜0) ∈ β„•)
9990, 98ffvelcdmd 7085 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ (Ξ›β€˜(π‘›β€˜0)) ∈ ℝ)
10033a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ 1 ∈ (0..^3))
10196, 100ffvelcdmd 7085 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ (π‘›β€˜1) ∈ β„•)
10290, 101ffvelcdmd 7085 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ (Ξ›β€˜(π‘›β€˜1)) ∈ ℝ)
10344a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ 2 ∈ (0..^3))
10496, 103ffvelcdmd 7085 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ {𝑑 ∈ (β„•(reprβ€˜3)𝑁) ∣ Β¬ (π‘‘β€˜0) ∈ (𝑂 ∩ β„™)}) β†’ (π‘›β€˜2) ∈ β„•)
10590, 104ffvelcdmd 7085 . . . . . . 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 472 . . . . . . . . 9 (4 ∈ ℝ ∧ 8 ∈ ℝ)
114 dp2cl 32034 . . . . . . . . 9 ((4 ∈ ℝ ∧ 8 ∈ ℝ) β†’ 48 ∈ ℝ)
115113, 114ax-mp 5 . . . . . . . 8 48 ∈ ℝ
11654, 115pm3.2i 472 . . . . . . 7 (3 ∈ ℝ ∧ 48 ∈ ℝ)
117 dp2cl 32034 . . . . . . 7 ((3 ∈ ℝ ∧ 48 ∈ ℝ) β†’ 348 ∈ ℝ)
118116, 117ax-mp 5 . . . . . 6 348 ∈ ℝ
119 dpcl 32045 . . . . . 6 ((7 ∈ β„•0 ∧ 348 ∈ ℝ) β†’ (7.348) ∈ ℝ)
12058, 118, 119mp2an 691 . . . . 5 (7.348) ∈ ℝ
121120a1i 11 . . . 4 (πœ‘ β†’ (7.348) ∈ ℝ)
1221nnrpd 13011 . . . . . 6 (πœ‘ β†’ 𝑁 ∈ ℝ+)
123122relogcld 26123 . . . . 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 472 . . . . . . . . . . . . . . . . . 18 (5 ∈ ℝ ∧ 5 ∈ ℝ)
138 dp2cl 32034 . . . . . . . . . . . . . . . . . 18 ((5 ∈ ℝ ∧ 5 ∈ ℝ) β†’ 55 ∈ ℝ)
139137, 138ax-mp 5 . . . . . . . . . . . . . . . . 17 55 ∈ ℝ
140135, 139pm3.2i 472 . . . . . . . . . . . . . . . 16 (9 ∈ ℝ ∧ 55 ∈ ℝ)
141 dp2cl 32034 . . . . . . . . . . . . . . . 16 ((9 ∈ ℝ ∧ 55 ∈ ℝ) β†’ 955 ∈ ℝ)
142140, 141ax-mp 5 . . . . . . . . . . . . . . 15 955 ∈ ℝ
143135, 142pm3.2i 472 . . . . . . . . . . . . . 14 (9 ∈ ℝ ∧ 955 ∈ ℝ)
144 dp2cl 32034 . . . . . . . . . . . . . 14 ((9 ∈ ℝ ∧ 955 ∈ ℝ) β†’ 9955 ∈ ℝ)
145143, 144ax-mp 5 . . . . . . . . . . . . 13 9955 ∈ ℝ
146134, 145pm3.2i 472 . . . . . . . . . . . 12 (7 ∈ ℝ ∧ 9955 ∈ ℝ)
147 dp2cl 32034 . . . . . . . . . . . 12 ((7 ∈ ℝ ∧ 9955 ∈ ℝ) β†’ 79955 ∈ ℝ)
148146, 147ax-mp 5 . . . . . . . . . . 11 79955 ∈ ℝ
149133, 148pm3.2i 472 . . . . . . . . . 10 (0 ∈ ℝ ∧ 79955 ∈ ℝ)
150 dp2cl 32034 . . . . . . . . . 10 ((0 ∈ ℝ ∧ 79955 ∈ ℝ) β†’ 079955 ∈ ℝ)
151149, 150ax-mp 5 . . . . . . . . 9 079955 ∈ ℝ
152 dpcl 32045 . . . . . . . . 9 ((1 ∈ β„•0 ∧ 079955 ∈ ℝ) β†’ (1.079955) ∈ ℝ)
15356, 151, 152mp2an 691 . . . . . . . 8 (1.079955) ∈ ℝ
154153a1i 11 . . . . . . 7 (πœ‘ β†’ (1.079955) ∈ ℝ)
155154resqcld 14087 . . . . . 6 (πœ‘ β†’ ((1.079955)↑2) ∈ ℝ)
156 1re 11211 . . . . . . . . . . . 12 1 ∈ ℝ
157156, 111pm3.2i 472 . . . . . . . . . . 11 (1 ∈ ℝ ∧ 4 ∈ ℝ)
158 dp2cl 32034 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 4 ∈ ℝ) β†’ 14 ∈ ℝ)
159157, 158ax-mp 5 . . . . . . . . . 10 14 ∈ ℝ
160111, 159pm3.2i 472 . . . . . . . . 9 (4 ∈ ℝ ∧ 14 ∈ ℝ)
161 dp2cl 32034 . . . . . . . . 9 ((4 ∈ ℝ ∧ 14 ∈ ℝ) β†’ 414 ∈ ℝ)
162160, 161ax-mp 5 . . . . . . . 8 414 ∈ ℝ
163 dpcl 32045 . . . . . . . 8 ((1 ∈ β„•0 ∧ 414 ∈ ℝ) β†’ (1.414) ∈ ℝ)
16456, 162, 163mp2an 691 . . . . . . 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 33654 . . . 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 17007 . . . . . . . . . 10 (10↑1) = 10
186179nn0rei 12480 . . . . . . . . . 10 10 ∈ ℝ
187185, 186eqeltri 2830 . . . . . . . . 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 5175 . . . . . . . . 9 2 ≀ (10↑1)
194193a1i 11 . . . . . . . 8 (πœ‘ β†’ 2 ≀ (10↑1))
195 1z 12589 . . . . . . . . . . . 12 1 ∈ β„€
196181nn0zi 12584 . . . . . . . . . . . 12 27 ∈ β„€
197186, 195, 1963pm3.2i 1340 . . . . . . . . . . 11 (10 ∈ ℝ ∧ 1 ∈ β„€ ∧ 27 ∈ β„€)
198 1lt10 12813 . . . . . . . . . . 11 1 < 10
199197, 198pm3.2i 472 . . . . . . . . . 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 478 . . . . . . . . . 10 ((((10 ∈ ℝ ∧ 1 ∈ β„€ ∧ 27 ∈ β„€) ∧ 1 < 10) ∧ 1 ≀ 27) β†’ (10↑1) ≀ (10↑27))
206199, 203, 205mp2an 691 . . . . . . . . 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 2733 . . . . . 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 33658 . . . . 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 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 13934 . . . . . . . . . . 11 (1...𝑁) ∈ Fin
230 diffi 9176 . . . . . . . . . . 11 ((1...𝑁) ∈ Fin β†’ ((1...𝑁) βˆ– β„™) ∈ Fin)
231229, 230ax-mp 5 . . . . . . . . . 10 ((1...𝑁) βˆ– β„™) ∈ Fin
232 snfi 9041 . . . . . . . . . 10 {2} ∈ Fin
233 unfi 9169 . . . . . . . . . 10 ((((1...𝑁) βˆ– β„™) ∈ Fin ∧ {2} ∈ Fin) β†’ (((1...𝑁) βˆ– β„™) βˆͺ {2}) ∈ Fin)
234231, 232, 233mp2an 691 . . . . . . . . 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 4142 . . . . . . . . . . 11 (πœ‘ β†’ ((1...𝑁) βˆ– β„™) βŠ† β„•)
240200a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ 2 ∈ β„•)
241240snssd 4812 . . . . . . . . . . 11 (πœ‘ β†’ {2} βŠ† β„•)
242239, 241unssd 4186 . . . . . . . . . 10 (πœ‘ β†’ (((1...𝑁) βˆ– β„™) βˆͺ {2}) βŠ† β„•)
243242sselda 3982 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})) β†’ 𝑖 ∈ β„•)
244236, 243ffvelcdmd 7085 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})) β†’ (Ξ›β€˜π‘–) ∈ ℝ)
245235, 244fsumrecl 15677 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) ∈ ℝ)
246 chpvalz 33629 . . . . . . . . 9 (𝑁 ∈ β„€ β†’ (Οˆβ€˜π‘) = Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))
24712, 246syl 17 . . . . . . . 8 (πœ‘ β†’ (Οˆβ€˜π‘) = Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))
248 chpf 26617 . . . . . . . . . 10 ψ:β„βŸΆβ„
249248a1i 11 . . . . . . . . 9 (πœ‘ β†’ ψ:β„βŸΆβ„)
250249, 124ffvelcdmd 7085 . . . . . . . 8 (πœ‘ β†’ (Οˆβ€˜π‘) ∈ ℝ)
251247, 250eqeltrrd 2835 . . . . . . 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 33657 . . . . 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 472 . . . . . . . . . . . . . . . 16 (6 ∈ ℝ ∧ 3 ∈ ℝ)
265 dp2cl 32034 . . . . . . . . . . . . . . . 16 ((6 ∈ ℝ ∧ 3 ∈ ℝ) β†’ 63 ∈ ℝ)
266264, 265ax-mp 5 . . . . . . . . . . . . . . 15 63 ∈ ℝ
267177, 266pm3.2i 472 . . . . . . . . . . . . . 14 (2 ∈ ℝ ∧ 63 ∈ ℝ)
268 dp2cl 32034 . . . . . . . . . . . . . 14 ((2 ∈ ℝ ∧ 63 ∈ ℝ) β†’ 263 ∈ ℝ)
269267, 268ax-mp 5 . . . . . . . . . . . . 13 263 ∈ ℝ
270111, 269pm3.2i 472 . . . . . . . . . . . 12 (4 ∈ ℝ ∧ 263 ∈ ℝ)
271 dp2cl 32034 . . . . . . . . . . . 12 ((4 ∈ ℝ ∧ 263 ∈ ℝ) β†’ 4263 ∈ ℝ)
272270, 271ax-mp 5 . . . . . . . . . . 11 4263 ∈ ℝ
273 dpcl 32045 . . . . . . . . . . 11 ((1 ∈ β„•0 ∧ 4263 ∈ ℝ) β†’ (1.4263) ∈ ℝ)
27456, 272, 273mp2an 691 . . . . . . . . . 10 (1.4263) ∈ ℝ
275274a1i 11 . . . . . . . . 9 (πœ‘ β†’ (1.4263) ∈ ℝ)
276275, 126remulcld 11241 . . . . . . . 8 (πœ‘ β†’ ((1.4263) Β· (βˆšβ€˜π‘)) ∈ ℝ)
277112, 54pm3.2i 472 . . . . . . . . . . . . . . . . . 18 (8 ∈ ℝ ∧ 3 ∈ ℝ)
278 dp2cl 32034 . . . . . . . . . . . . . . . . . 18 ((8 ∈ ℝ ∧ 3 ∈ ℝ) β†’ 83 ∈ ℝ)
279277, 278ax-mp 5 . . . . . . . . . . . . . . . . 17 83 ∈ ℝ
280112, 279pm3.2i 472 . . . . . . . . . . . . . . . 16 (8 ∈ ℝ ∧ 83 ∈ ℝ)
281 dp2cl 32034 . . . . . . . . . . . . . . . 16 ((8 ∈ ℝ ∧ 83 ∈ ℝ) β†’ 883 ∈ ℝ)
282280, 281ax-mp 5 . . . . . . . . . . . . . . 15 883 ∈ ℝ
28354, 282pm3.2i 472 . . . . . . . . . . . . . 14 (3 ∈ ℝ ∧ 883 ∈ ℝ)
284 dp2cl 32034 . . . . . . . . . . . . . 14 ((3 ∈ ℝ ∧ 883 ∈ ℝ) β†’ 3883 ∈ ℝ)
285283, 284ax-mp 5 . . . . . . . . . . . . 13 3883 ∈ ℝ
286133, 285pm3.2i 472 . . . . . . . . . . . 12 (0 ∈ ℝ ∧ 3883 ∈ ℝ)
287 dp2cl 32034 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ 3883 ∈ ℝ) β†’ 03883 ∈ ℝ)
288286, 287ax-mp 5 . . . . . . . . . . 11 03883 ∈ ℝ
289 dpcl 32045 . . . . . . . . . . 11 ((1 ∈ β„•0 ∧ 03883 ∈ ℝ) β†’ (1.03883) ∈ ℝ)
29056, 288, 289mp2an 691 . . . . . . . . . 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 26615 . . . . . . . . . . 11 (𝑖 ∈ β„• β†’ 0 ≀ (Ξ›β€˜π‘–))
298243, 297syl 17 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})) β†’ 0 ≀ (Ξ›β€˜π‘–))
299235, 244, 298fsumge0 15738 . . . . . . . . 9 (πœ‘ β†’ 0 ≀ Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–))
3001, 209hgt750lemd 33649 . . . . . . . . 9 (πœ‘ β†’ Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) < ((1.4263) Β· (βˆšβ€˜π‘)))
301 fzfid 13935 . . . . . . . . . 10 (πœ‘ β†’ (1...𝑁) ∈ Fin)
3029a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ (1...𝑁)) β†’ Ξ›:β„•βŸΆβ„)
303238sselda 3982 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ (1...𝑁)) β†’ 𝑗 ∈ β„•)
304302, 303ffvelcdmd 7085 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (1...𝑁)) β†’ (Ξ›β€˜π‘—) ∈ ℝ)
305 vmage0 26615 . . . . . . . . . . 11 (𝑗 ∈ β„• β†’ 0 ≀ (Ξ›β€˜π‘—))
306303, 305syl 17 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (1...𝑁)) β†’ 0 ≀ (Ξ›β€˜π‘—))
307301, 304, 306fsumge0 15738 . . . . . . . . 9 (πœ‘ β†’ 0 ≀ Σ𝑗 ∈ (1...𝑁)(Ξ›β€˜π‘—))
3081hgt750lemc 33648 . . . . . . . . 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 26129 . . . . . . . 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 33653 . . . . . . 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 7422 . . . . . . . . . . . 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 2773 . . . . . . . . . . 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 2773 . . . . . . . . . 10 (πœ‘ β†’ ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁))) = (((1.4263) Β· (1.03883)) Β· (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘))))
349348oveq2d 7422 . . . . . . . . 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 2776 . . . . . . . 8 (πœ‘ β†’ ((((1.079955)↑2) Β· (1.414)) Β· ((logβ€˜π‘) Β· (((1.4263) Β· (βˆšβ€˜π‘)) Β· ((1.03883) Β· 𝑁)))) = (((((1.079955)↑2) Β· (1.414)) Β· ((1.4263) Β· (1.03883))) Β· (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘))))
354353oveq2d 7422 . . . . . . 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 2776 . . . . . 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 7421 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑁↑2) / (βˆšβ€˜π‘)) = ((𝑁 Β· 𝑁) / (βˆšβ€˜π‘)))
365338, 338, 336, 128divassd 12022 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑁 Β· 𝑁) / (βˆšβ€˜π‘)) = (𝑁 Β· (𝑁 / (βˆšβ€˜π‘))))
366 divsqrtid 33595 . . . . . . . . . . . . 13 (𝑁 ∈ ℝ+ β†’ (𝑁 / (βˆšβ€˜π‘)) = (βˆšβ€˜π‘))
367122, 366syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑁 / (βˆšβ€˜π‘)) = (βˆšβ€˜π‘))
368367oveq2d 7422 . . . . . . . . . . 11 (πœ‘ β†’ (𝑁 Β· (𝑁 / (βˆšβ€˜π‘))) = (𝑁 Β· (βˆšβ€˜π‘)))
369364, 365, 3683eqtrd 2777 . . . . . . . . . 10 (πœ‘ β†’ ((𝑁↑2) / (βˆšβ€˜π‘)) = (𝑁 Β· (βˆšβ€˜π‘)))
370338, 336mulcomd 11232 . . . . . . . . . 10 (πœ‘ β†’ (𝑁 Β· (βˆšβ€˜π‘)) = ((βˆšβ€˜π‘) Β· 𝑁))
371369, 370eqtrd 2773 . . . . . . . . 9 (πœ‘ β†’ ((𝑁↑2) / (βˆšβ€˜π‘)) = ((βˆšβ€˜π‘) Β· 𝑁))
372371oveq1d 7421 . . . . . . . 8 (πœ‘ β†’ (((𝑁↑2) / (βˆšβ€˜π‘)) Β· (logβ€˜π‘)) = (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘)))
373360, 362, 3723eqtrrd 2778 . . . . . . 7 (πœ‘ β†’ (((βˆšβ€˜π‘) Β· 𝑁) Β· (logβ€˜π‘)) = (((logβ€˜π‘) / (βˆšβ€˜π‘)) Β· (𝑁↑2)))
374373oveq2d 7422 . . . . . 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 2773 . . . . 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 5180 . . . 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 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  {crab 3433   βˆ– 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 6537  β€˜cfv 6541  (class class class)co 7406  Fincfn 8936  β„‚cc 11105  β„cr 11106  0cc0 11107  1c1 11108   Β· cmul 11112  +∞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 19304  logclog 26055  Ξ›cvma 26586  Οˆcchp 26587  cdp2 32025  .cdp 32042  reprcrepr 33609
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-reg 9584  ax-inf2 9633  ax-ac2 10455  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185  ax-addf 11186  ax-mulf 11187  ax-ros335 33646  ax-ros336 33647
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  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 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-of 7667  df-om 7853  df-1st 7972  df-2nd 7973  df-supp 8144  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-2o 8464  df-oadd 8467  df-er 8700  df-map 8819  df-pm 8820  df-ixp 8889  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fsupp 9359  df-fi 9403  df-sup 9434  df-inf 9435  df-oi 9502  df-r1 9756  df-rank 9757  df-dju 9893  df-card 9931  df-ac 10108  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 16767  df-struct 17077  df-sets 17094  df-slot 17112  df-ndx 17124  df-base 17142  df-ress 17171  df-plusg 17207  df-mulr 17208  df-starv 17209  df-sca 17210  df-vsca 17211  df-ip 17212  df-tset 17213  df-ple 17214  df-ds 17216  df-unif 17217  df-hom 17218  df-cco 17219  df-rest 17365  df-topn 17366  df-0g 17384  df-gsum 17385  df-topgen 17386  df-pt 17387  df-prds 17390  df-xrs 17445  df-qtop 17450  df-imas 17451  df-xps 17453  df-mre 17527  df-mrc 17528  df-acs 17530  df-mgm 18558  df-sgrp 18607  df-mnd 18623  df-submnd 18669  df-mulg 18946  df-cntz 19176  df-pmtr 19305  df-cmn 19645  df-psmet 20929  df-xmet 20930  df-met 20931  df-bl 20932  df-mopn 20933  df-fbas 20934  df-fg 20935  df-cnfld 20938  df-top 22388  df-topon 22405  df-topsp 22427  df-bases 22441  df-cld 22515  df-ntr 22516  df-cls 22517  df-nei 22594  df-lp 22632  df-perf 22633  df-cn 22723  df-cnp 22724  df-haus 22811  df-cmp 22883  df-tx 23058  df-hmeo 23251  df-fil 23342  df-fm 23434  df-flim 23435  df-flf 23436  df-xms 23818  df-ms 23819  df-tms 23820  df-cncf 24386  df-limc 25375  df-dv 25376  df-ulm 25881  df-log 26057  df-atan 26362  df-cht 26591  df-vma 26592  df-chp 26593  df-dp2 32026  df-dp 32043  df-repr 33610
This theorem is referenced by:  tgoldbachgtde  33661
  Copyright terms: Public domain W3C validator