MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  chtppilimlem2 Structured version   Visualization version   GIF version

Theorem chtppilimlem2 27394
Description: Lemma for chtppilim 27395. (Contributed by Mario Carneiro, 22-Sep-2014.)
Hypotheses
Ref Expression
chtppilim.1 (πœ‘ β†’ 𝐴 ∈ ℝ+)
chtppilim.2 (πœ‘ β†’ 𝐴 < 1)
Assertion
Ref Expression
chtppilimlem2 (πœ‘ β†’ βˆƒπ‘§ ∈ ℝ βˆ€π‘₯ ∈ (2[,)+∞)(𝑧 ≀ π‘₯ β†’ ((𝐴↑2) Β· ((Ο€β€˜π‘₯) Β· (logβ€˜π‘₯))) < (ΞΈβ€˜π‘₯)))
Distinct variable groups:   π‘₯,𝑧,𝐴   πœ‘,π‘₯,𝑧

Proof of Theorem chtppilimlem2
StepHypRef Expression
1 simpr 484 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ π‘₯ ∈ (2[,)+∞))
2 2re 12308 . . . . . . . . . 10 2 ∈ ℝ
3 elicopnf 13446 . . . . . . . . . 10 (2 ∈ ℝ β†’ (π‘₯ ∈ (2[,)+∞) ↔ (π‘₯ ∈ ℝ ∧ 2 ≀ π‘₯)))
42, 3ax-mp 5 . . . . . . . . 9 (π‘₯ ∈ (2[,)+∞) ↔ (π‘₯ ∈ ℝ ∧ 2 ≀ π‘₯))
51, 4sylib 217 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (π‘₯ ∈ ℝ ∧ 2 ≀ π‘₯))
65simpld 494 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ π‘₯ ∈ ℝ)
7 0red 11239 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ 0 ∈ ℝ)
82a1i 11 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ 2 ∈ ℝ)
9 2pos 12337 . . . . . . . . 9 0 < 2
109a1i 11 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ 0 < 2)
115simprd 495 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ 2 ≀ π‘₯)
127, 8, 6, 10, 11ltletrd 11396 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ 0 < π‘₯)
136, 12elrpd 13037 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ π‘₯ ∈ ℝ+)
14 chtppilim.1 . . . . . . . 8 (πœ‘ β†’ 𝐴 ∈ ℝ+)
1514rpred 13040 . . . . . . 7 (πœ‘ β†’ 𝐴 ∈ ℝ)
1615adantr 480 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ 𝐴 ∈ ℝ)
1713, 16rpcxpcld 26654 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (π‘₯↑𝑐𝐴) ∈ ℝ+)
18 ppinncl 27093 . . . . . . 7 ((π‘₯ ∈ ℝ ∧ 2 ≀ π‘₯) β†’ (Ο€β€˜π‘₯) ∈ β„•)
195, 18syl 17 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (Ο€β€˜π‘₯) ∈ β„•)
2019nnrpd 13038 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (Ο€β€˜π‘₯) ∈ ℝ+)
2117, 20rpdivcld 13057 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ ((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)) ∈ ℝ+)
2221ralrimiva 3141 . . 3 (πœ‘ β†’ βˆ€π‘₯ ∈ (2[,)+∞)((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)) ∈ ℝ+)
23 chtppilim.2 . . . 4 (πœ‘ β†’ 𝐴 < 1)
24 1re 11236 . . . . 5 1 ∈ ℝ
25 difrp 13036 . . . . 5 ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) β†’ (𝐴 < 1 ↔ (1 βˆ’ 𝐴) ∈ ℝ+))
2615, 24, 25sylancl 585 . . . 4 (πœ‘ β†’ (𝐴 < 1 ↔ (1 βˆ’ 𝐴) ∈ ℝ+))
2723, 26mpbid 231 . . 3 (πœ‘ β†’ (1 βˆ’ 𝐴) ∈ ℝ+)
28 ovexd 7449 . . . . . 6 (πœ‘ β†’ (2[,)+∞) ∈ V)
2924a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ 1 ∈ ℝ)
30 1lt2 12405 . . . . . . . . . . 11 1 < 2
3130a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ 1 < 2)
3229, 8, 6, 31, 11ltletrd 11396 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ 1 < π‘₯)
336, 32rplogcld 26550 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (logβ€˜π‘₯) ∈ ℝ+)
3413, 33rpdivcld 13057 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (π‘₯ / (logβ€˜π‘₯)) ∈ ℝ+)
3534, 20rpdivcld 13057 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ ((π‘₯ / (logβ€˜π‘₯)) / (Ο€β€˜π‘₯)) ∈ ℝ+)
3627adantr 480 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (1 βˆ’ 𝐴) ∈ ℝ+)
3736rpred 13040 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (1 βˆ’ 𝐴) ∈ ℝ)
3813, 37rpcxpcld 26654 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (π‘₯↑𝑐(1 βˆ’ 𝐴)) ∈ ℝ+)
3933, 38rpdivcld 13057 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴))) ∈ ℝ+)
40 eqidd 2728 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ (2[,)+∞) ↦ ((π‘₯ / (logβ€˜π‘₯)) / (Ο€β€˜π‘₯))) = (π‘₯ ∈ (2[,)+∞) ↦ ((π‘₯ / (logβ€˜π‘₯)) / (Ο€β€˜π‘₯))))
41 eqidd 2728 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ (2[,)+∞) ↦ ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴)))) = (π‘₯ ∈ (2[,)+∞) ↦ ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴)))))
4228, 35, 39, 40, 41offval2 7699 . . . . 5 (πœ‘ β†’ ((π‘₯ ∈ (2[,)+∞) ↦ ((π‘₯ / (logβ€˜π‘₯)) / (Ο€β€˜π‘₯))) ∘f Β· (π‘₯ ∈ (2[,)+∞) ↦ ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴))))) = (π‘₯ ∈ (2[,)+∞) ↦ (((π‘₯ / (logβ€˜π‘₯)) / (Ο€β€˜π‘₯)) Β· ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴))))))
4334rpcnd 13042 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (π‘₯ / (logβ€˜π‘₯)) ∈ β„‚)
4439rpcnd 13042 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴))) ∈ β„‚)
4520rpcnne0d 13049 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ ((Ο€β€˜π‘₯) ∈ β„‚ ∧ (Ο€β€˜π‘₯) β‰  0))
46 div23 11913 . . . . . . . 8 (((π‘₯ / (logβ€˜π‘₯)) ∈ β„‚ ∧ ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴))) ∈ β„‚ ∧ ((Ο€β€˜π‘₯) ∈ β„‚ ∧ (Ο€β€˜π‘₯) β‰  0)) β†’ (((π‘₯ / (logβ€˜π‘₯)) Β· ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴)))) / (Ο€β€˜π‘₯)) = (((π‘₯ / (logβ€˜π‘₯)) / (Ο€β€˜π‘₯)) Β· ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴)))))
4743, 44, 45, 46syl3anc 1369 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (((π‘₯ / (logβ€˜π‘₯)) Β· ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴)))) / (Ο€β€˜π‘₯)) = (((π‘₯ / (logβ€˜π‘₯)) / (Ο€β€˜π‘₯)) Β· ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴)))))
4833rpcnne0d 13049 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ ((logβ€˜π‘₯) ∈ β„‚ ∧ (logβ€˜π‘₯) β‰  0))
4938rpcnne0d 13049 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ ((π‘₯↑𝑐(1 βˆ’ 𝐴)) ∈ β„‚ ∧ (π‘₯↑𝑐(1 βˆ’ 𝐴)) β‰  0))
506recnd 11264 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ π‘₯ ∈ β„‚)
51 dmdcan 11946 . . . . . . . . . 10 ((((logβ€˜π‘₯) ∈ β„‚ ∧ (logβ€˜π‘₯) β‰  0) ∧ ((π‘₯↑𝑐(1 βˆ’ 𝐴)) ∈ β„‚ ∧ (π‘₯↑𝑐(1 βˆ’ 𝐴)) β‰  0) ∧ π‘₯ ∈ β„‚) β†’ (((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴))) Β· (π‘₯ / (logβ€˜π‘₯))) = (π‘₯ / (π‘₯↑𝑐(1 βˆ’ 𝐴))))
5248, 49, 50, 51syl3anc 1369 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴))) Β· (π‘₯ / (logβ€˜π‘₯))) = (π‘₯ / (π‘₯↑𝑐(1 βˆ’ 𝐴))))
5343, 44mulcomd 11257 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ ((π‘₯ / (logβ€˜π‘₯)) Β· ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴)))) = (((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴))) Β· (π‘₯ / (logβ€˜π‘₯))))
5413rpcnne0d 13049 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (π‘₯ ∈ β„‚ ∧ π‘₯ β‰  0))
55 ax-1cn 11188 . . . . . . . . . . . . 13 1 ∈ β„‚
5655a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ 1 ∈ β„‚)
5736rpcnd 13042 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (1 βˆ’ 𝐴) ∈ β„‚)
58 cxpsub 26603 . . . . . . . . . . . 12 (((π‘₯ ∈ β„‚ ∧ π‘₯ β‰  0) ∧ 1 ∈ β„‚ ∧ (1 βˆ’ 𝐴) ∈ β„‚) β†’ (π‘₯↑𝑐(1 βˆ’ (1 βˆ’ 𝐴))) = ((π‘₯↑𝑐1) / (π‘₯↑𝑐(1 βˆ’ 𝐴))))
5954, 56, 57, 58syl3anc 1369 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (π‘₯↑𝑐(1 βˆ’ (1 βˆ’ 𝐴))) = ((π‘₯↑𝑐1) / (π‘₯↑𝑐(1 βˆ’ 𝐴))))
6016recnd 11264 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ 𝐴 ∈ β„‚)
61 nncan 11511 . . . . . . . . . . . . 13 ((1 ∈ β„‚ ∧ 𝐴 ∈ β„‚) β†’ (1 βˆ’ (1 βˆ’ 𝐴)) = 𝐴)
6255, 60, 61sylancr 586 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (1 βˆ’ (1 βˆ’ 𝐴)) = 𝐴)
6362oveq2d 7430 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (π‘₯↑𝑐(1 βˆ’ (1 βˆ’ 𝐴))) = (π‘₯↑𝑐𝐴))
6459, 63eqtr3d 2769 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ ((π‘₯↑𝑐1) / (π‘₯↑𝑐(1 βˆ’ 𝐴))) = (π‘₯↑𝑐𝐴))
6550cxp1d 26627 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (π‘₯↑𝑐1) = π‘₯)
6665oveq1d 7429 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ ((π‘₯↑𝑐1) / (π‘₯↑𝑐(1 βˆ’ 𝐴))) = (π‘₯ / (π‘₯↑𝑐(1 βˆ’ 𝐴))))
6764, 66eqtr3d 2769 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (π‘₯↑𝑐𝐴) = (π‘₯ / (π‘₯↑𝑐(1 βˆ’ 𝐴))))
6852, 53, 673eqtr4d 2777 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ ((π‘₯ / (logβ€˜π‘₯)) Β· ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴)))) = (π‘₯↑𝑐𝐴))
6968oveq1d 7429 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (((π‘₯ / (logβ€˜π‘₯)) Β· ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴)))) / (Ο€β€˜π‘₯)) = ((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)))
7047, 69eqtr3d 2769 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (((π‘₯ / (logβ€˜π‘₯)) / (Ο€β€˜π‘₯)) Β· ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴)))) = ((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)))
7170mpteq2dva 5242 . . . . 5 (πœ‘ β†’ (π‘₯ ∈ (2[,)+∞) ↦ (((π‘₯ / (logβ€˜π‘₯)) / (Ο€β€˜π‘₯)) Β· ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴))))) = (π‘₯ ∈ (2[,)+∞) ↦ ((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯))))
7242, 71eqtrd 2767 . . . 4 (πœ‘ β†’ ((π‘₯ ∈ (2[,)+∞) ↦ ((π‘₯ / (logβ€˜π‘₯)) / (Ο€β€˜π‘₯))) ∘f Β· (π‘₯ ∈ (2[,)+∞) ↦ ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴))))) = (π‘₯ ∈ (2[,)+∞) ↦ ((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯))))
73 chebbnd1 27392 . . . . 5 (π‘₯ ∈ (2[,)+∞) ↦ ((π‘₯ / (logβ€˜π‘₯)) / (Ο€β€˜π‘₯))) ∈ 𝑂(1)
7413ex 412 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ (2[,)+∞) β†’ π‘₯ ∈ ℝ+))
7574ssrdv 3984 . . . . . 6 (πœ‘ β†’ (2[,)+∞) βŠ† ℝ+)
76 cxploglim 26897 . . . . . . 7 ((1 βˆ’ 𝐴) ∈ ℝ+ β†’ (π‘₯ ∈ ℝ+ ↦ ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴)))) β‡π‘Ÿ 0)
7727, 76syl 17 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ ℝ+ ↦ ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴)))) β‡π‘Ÿ 0)
7875, 77rlimres2 15529 . . . . 5 (πœ‘ β†’ (π‘₯ ∈ (2[,)+∞) ↦ ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴)))) β‡π‘Ÿ 0)
79 o1rlimmul 15587 . . . . 5 (((π‘₯ ∈ (2[,)+∞) ↦ ((π‘₯ / (logβ€˜π‘₯)) / (Ο€β€˜π‘₯))) ∈ 𝑂(1) ∧ (π‘₯ ∈ (2[,)+∞) ↦ ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴)))) β‡π‘Ÿ 0) β†’ ((π‘₯ ∈ (2[,)+∞) ↦ ((π‘₯ / (logβ€˜π‘₯)) / (Ο€β€˜π‘₯))) ∘f Β· (π‘₯ ∈ (2[,)+∞) ↦ ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴))))) β‡π‘Ÿ 0)
8073, 78, 79sylancr 586 . . . 4 (πœ‘ β†’ ((π‘₯ ∈ (2[,)+∞) ↦ ((π‘₯ / (logβ€˜π‘₯)) / (Ο€β€˜π‘₯))) ∘f Β· (π‘₯ ∈ (2[,)+∞) ↦ ((logβ€˜π‘₯) / (π‘₯↑𝑐(1 βˆ’ 𝐴))))) β‡π‘Ÿ 0)
8172, 80eqbrtrrd 5166 . . 3 (πœ‘ β†’ (π‘₯ ∈ (2[,)+∞) ↦ ((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯))) β‡π‘Ÿ 0)
8222, 27, 81rlimi 15481 . 2 (πœ‘ β†’ βˆƒπ‘§ ∈ ℝ βˆ€π‘₯ ∈ (2[,)+∞)(𝑧 ≀ π‘₯ β†’ (absβ€˜(((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)) βˆ’ 0)) < (1 βˆ’ 𝐴)))
8321rpcnd 13042 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ ((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)) ∈ β„‚)
8483subid1d 11582 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)) βˆ’ 0) = ((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)))
8584fveq2d 6895 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (absβ€˜(((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)) βˆ’ 0)) = (absβ€˜((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯))))
8621rpred 13040 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ ((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)) ∈ ℝ)
8721rpge0d 13044 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ 0 ≀ ((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)))
8886, 87absidd 15393 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (absβ€˜((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯))) = ((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)))
8985, 88eqtrd 2767 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (absβ€˜(((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)) βˆ’ 0)) = ((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)))
9089breq1d 5152 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ ((absβ€˜(((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)) βˆ’ 0)) < (1 βˆ’ 𝐴) ↔ ((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)) < (1 βˆ’ 𝐴)))
9114adantr 480 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (2[,)+∞) ∧ ((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)) < (1 βˆ’ 𝐴))) β†’ 𝐴 ∈ ℝ+)
9223adantr 480 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (2[,)+∞) ∧ ((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)) < (1 βˆ’ 𝐴))) β†’ 𝐴 < 1)
93 simprl 770 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (2[,)+∞) ∧ ((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)) < (1 βˆ’ 𝐴))) β†’ π‘₯ ∈ (2[,)+∞))
94 simprr 772 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (2[,)+∞) ∧ ((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)) < (1 βˆ’ 𝐴))) β†’ ((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)) < (1 βˆ’ 𝐴))
9591, 92, 93, 94chtppilimlem1 27393 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (2[,)+∞) ∧ ((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)) < (1 βˆ’ 𝐴))) β†’ ((𝐴↑2) Β· ((Ο€β€˜π‘₯) Β· (logβ€˜π‘₯))) < (ΞΈβ€˜π‘₯))
9695expr 456 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ (((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)) < (1 βˆ’ 𝐴) β†’ ((𝐴↑2) Β· ((Ο€β€˜π‘₯) Β· (logβ€˜π‘₯))) < (ΞΈβ€˜π‘₯)))
9790, 96sylbid 239 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ ((absβ€˜(((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)) βˆ’ 0)) < (1 βˆ’ 𝐴) β†’ ((𝐴↑2) Β· ((Ο€β€˜π‘₯) Β· (logβ€˜π‘₯))) < (ΞΈβ€˜π‘₯)))
9897imim2d 57 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (2[,)+∞)) β†’ ((𝑧 ≀ π‘₯ β†’ (absβ€˜(((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)) βˆ’ 0)) < (1 βˆ’ 𝐴)) β†’ (𝑧 ≀ π‘₯ β†’ ((𝐴↑2) Β· ((Ο€β€˜π‘₯) Β· (logβ€˜π‘₯))) < (ΞΈβ€˜π‘₯))))
9998ralimdva 3162 . . 3 (πœ‘ β†’ (βˆ€π‘₯ ∈ (2[,)+∞)(𝑧 ≀ π‘₯ β†’ (absβ€˜(((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)) βˆ’ 0)) < (1 βˆ’ 𝐴)) β†’ βˆ€π‘₯ ∈ (2[,)+∞)(𝑧 ≀ π‘₯ β†’ ((𝐴↑2) Β· ((Ο€β€˜π‘₯) Β· (logβ€˜π‘₯))) < (ΞΈβ€˜π‘₯))))
10099reximdv 3165 . 2 (πœ‘ β†’ (βˆƒπ‘§ ∈ ℝ βˆ€π‘₯ ∈ (2[,)+∞)(𝑧 ≀ π‘₯ β†’ (absβ€˜(((π‘₯↑𝑐𝐴) / (Ο€β€˜π‘₯)) βˆ’ 0)) < (1 βˆ’ 𝐴)) β†’ βˆƒπ‘§ ∈ ℝ βˆ€π‘₯ ∈ (2[,)+∞)(𝑧 ≀ π‘₯ β†’ ((𝐴↑2) Β· ((Ο€β€˜π‘₯) Β· (logβ€˜π‘₯))) < (ΞΈβ€˜π‘₯))))
10182, 100mpd 15 1 (πœ‘ β†’ βˆƒπ‘§ ∈ ℝ βˆ€π‘₯ ∈ (2[,)+∞)(𝑧 ≀ π‘₯ β†’ ((𝐴↑2) Β· ((Ο€β€˜π‘₯) Β· (logβ€˜π‘₯))) < (ΞΈβ€˜π‘₯)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1534   ∈ wcel 2099   β‰  wne 2935  βˆ€wral 3056  βˆƒwrex 3065  Vcvv 3469   class class class wbr 5142   ↦ cmpt 5225  β€˜cfv 6542  (class class class)co 7414   ∘f cof 7677  β„‚cc 11128  β„cr 11129  0cc0 11130  1c1 11131   Β· cmul 11135  +∞cpnf 11267   < clt 11270   ≀ cle 11271   βˆ’ cmin 11466   / cdiv 11893  β„•cn 12234  2c2 12289  β„+crp 12998  [,)cico 13350  β†‘cexp 14050  abscabs 15205   β‡π‘Ÿ crli 15453  π‘‚(1)co1 15454  logclog 26475  β†‘𝑐ccxp 26476  ΞΈccht 27010  Ο€cppi 27013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-inf2 9656  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208  ax-addf 11209
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-om 7865  df-1st 7987  df-2nd 7988  df-supp 8160  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-oadd 8484  df-er 8718  df-map 8838  df-pm 8839  df-ixp 8908  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fsupp 9378  df-fi 9426  df-sup 9457  df-inf 9458  df-oi 9525  df-dju 9916  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-4 12299  df-5 12300  df-6 12301  df-7 12302  df-8 12303  df-9 12304  df-n0 12495  df-xnn0 12567  df-z 12581  df-dec 12700  df-uz 12845  df-q 12955  df-rp 12999  df-xneg 13116  df-xadd 13117  df-xmul 13118  df-ioo 13352  df-ioc 13353  df-ico 13354  df-icc 13355  df-fz 13509  df-fzo 13652  df-fl 13781  df-mod 13859  df-seq 13991  df-exp 14051  df-fac 14257  df-bc 14286  df-hash 14314  df-shft 15038  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-limsup 15439  df-clim 15456  df-rlim 15457  df-o1 15458  df-lo1 15459  df-sum 15657  df-ef 16035  df-e 16036  df-sin 16037  df-cos 16038  df-pi 16040  df-dvds 16223  df-gcd 16461  df-prm 16634  df-pc 16797  df-struct 17107  df-sets 17124  df-slot 17142  df-ndx 17154  df-base 17172  df-ress 17201  df-plusg 17237  df-mulr 17238  df-starv 17239  df-sca 17240  df-vsca 17241  df-ip 17242  df-tset 17243  df-ple 17244  df-ds 17246  df-unif 17247  df-hom 17248  df-cco 17249  df-rest 17395  df-topn 17396  df-0g 17414  df-gsum 17415  df-topgen 17416  df-pt 17417  df-prds 17420  df-xrs 17475  df-qtop 17480  df-imas 17481  df-xps 17483  df-mre 17557  df-mrc 17558  df-acs 17560  df-mgm 18591  df-sgrp 18670  df-mnd 18686  df-submnd 18732  df-mulg 19015  df-cntz 19259  df-cmn 19728  df-psmet 21258  df-xmet 21259  df-met 21260  df-bl 21261  df-mopn 21262  df-fbas 21263  df-fg 21264  df-cnfld 21267  df-top 22783  df-topon 22800  df-topsp 22822  df-bases 22836  df-cld 22910  df-ntr 22911  df-cls 22912  df-nei 22989  df-lp 23027  df-perf 23028  df-cn 23118  df-cnp 23119  df-haus 23206  df-tx 23453  df-hmeo 23646  df-fil 23737  df-fm 23829  df-flim 23830  df-flf 23831  df-xms 24213  df-ms 24214  df-tms 24215  df-cncf 24785  df-limc 25782  df-dv 25783  df-log 26477  df-cxp 26478  df-cht 27016  df-ppi 27019
This theorem is referenced by:  chtppilim  27395
  Copyright terms: Public domain W3C validator