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

Theorem bposlem7 25309
Description: Lemma for bpos 25312. The function 𝐹 is decreasing. (Contributed by Mario Carneiro, 13-Mar-2014.)
Hypotheses
Ref Expression
bposlem7.1 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))
bposlem7.2 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))
bposlem7.3 (𝜑𝐴 ∈ ℕ)
bposlem7.4 (𝜑𝐵 ∈ ℕ)
bposlem7.5 (𝜑 → (e↑2) ≤ 𝐴)
bposlem7.6 (𝜑 → (e↑2) ≤ 𝐵)
Assertion
Ref Expression
bposlem7 (𝜑 → (𝐴 < 𝐵 → (𝐹𝐵) < (𝐹𝐴)))
Distinct variable groups:   𝐴,𝑛   𝐵,𝑛   𝑛,𝐺   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥,𝑛)   𝐹(𝑥,𝑛)   𝐺(𝑥)

Proof of Theorem bposlem7
StepHypRef Expression
1 bposlem7.4 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℕ)
21nnrpd 12071 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℝ+)
32rpsqrtcld 14438 . . . . . . . . . . 11 (𝜑 → (√‘𝐵) ∈ ℝ+)
4 fveq2 6377 . . . . . . . . . . . . 13 (𝑥 = (√‘𝐵) → (log‘𝑥) = (log‘(√‘𝐵)))
5 id 22 . . . . . . . . . . . . 13 (𝑥 = (√‘𝐵) → 𝑥 = (√‘𝐵))
64, 5oveq12d 6862 . . . . . . . . . . . 12 (𝑥 = (√‘𝐵) → ((log‘𝑥) / 𝑥) = ((log‘(√‘𝐵)) / (√‘𝐵)))
7 bposlem7.2 . . . . . . . . . . . 12 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))
8 ovex 6876 . . . . . . . . . . . 12 ((log‘(√‘𝐵)) / (√‘𝐵)) ∈ V
96, 7, 8fvmpt 6473 . . . . . . . . . . 11 ((√‘𝐵) ∈ ℝ+ → (𝐺‘(√‘𝐵)) = ((log‘(√‘𝐵)) / (√‘𝐵)))
103, 9syl 17 . . . . . . . . . 10 (𝜑 → (𝐺‘(√‘𝐵)) = ((log‘(√‘𝐵)) / (√‘𝐵)))
11 bposlem7.3 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℕ)
1211nnrpd 12071 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℝ+)
1312rpsqrtcld 14438 . . . . . . . . . . 11 (𝜑 → (√‘𝐴) ∈ ℝ+)
14 fveq2 6377 . . . . . . . . . . . . 13 (𝑥 = (√‘𝐴) → (log‘𝑥) = (log‘(√‘𝐴)))
15 id 22 . . . . . . . . . . . . 13 (𝑥 = (√‘𝐴) → 𝑥 = (√‘𝐴))
1614, 15oveq12d 6862 . . . . . . . . . . . 12 (𝑥 = (√‘𝐴) → ((log‘𝑥) / 𝑥) = ((log‘(√‘𝐴)) / (√‘𝐴)))
17 ovex 6876 . . . . . . . . . . . 12 ((log‘(√‘𝐴)) / (√‘𝐴)) ∈ V
1816, 7, 17fvmpt 6473 . . . . . . . . . . 11 ((√‘𝐴) ∈ ℝ+ → (𝐺‘(√‘𝐴)) = ((log‘(√‘𝐴)) / (√‘𝐴)))
1913, 18syl 17 . . . . . . . . . 10 (𝜑 → (𝐺‘(√‘𝐴)) = ((log‘(√‘𝐴)) / (√‘𝐴)))
2010, 19breq12d 4824 . . . . . . . . 9 (𝜑 → ((𝐺‘(√‘𝐵)) < (𝐺‘(√‘𝐴)) ↔ ((log‘(√‘𝐵)) / (√‘𝐵)) < ((log‘(√‘𝐴)) / (√‘𝐴))))
2113rpred 12073 . . . . . . . . . 10 (𝜑 → (√‘𝐴) ∈ ℝ)
22 bposlem7.5 . . . . . . . . . . . 12 (𝜑 → (e↑2) ≤ 𝐴)
2312rprege0d 12080 . . . . . . . . . . . . 13 (𝜑 → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
24 resqrtth 14284 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√‘𝐴)↑2) = 𝐴)
2523, 24syl 17 . . . . . . . . . . . 12 (𝜑 → ((√‘𝐴)↑2) = 𝐴)
2622, 25breqtrrd 4839 . . . . . . . . . . 11 (𝜑 → (e↑2) ≤ ((√‘𝐴)↑2))
2713rpge0d 12077 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (√‘𝐴))
28 ere 15104 . . . . . . . . . . . . 13 e ∈ ℝ
29 0re 10297 . . . . . . . . . . . . . 14 0 ∈ ℝ
30 epos 15220 . . . . . . . . . . . . . 14 0 < e
3129, 28, 30ltleii 10416 . . . . . . . . . . . . 13 0 ≤ e
32 le2sq 13148 . . . . . . . . . . . . 13 (((e ∈ ℝ ∧ 0 ≤ e) ∧ ((√‘𝐴) ∈ ℝ ∧ 0 ≤ (√‘𝐴))) → (e ≤ (√‘𝐴) ↔ (e↑2) ≤ ((√‘𝐴)↑2)))
3328, 31, 32mpanl12 693 . . . . . . . . . . . 12 (((√‘𝐴) ∈ ℝ ∧ 0 ≤ (√‘𝐴)) → (e ≤ (√‘𝐴) ↔ (e↑2) ≤ ((√‘𝐴)↑2)))
3421, 27, 33syl2anc 579 . . . . . . . . . . 11 (𝜑 → (e ≤ (√‘𝐴) ↔ (e↑2) ≤ ((√‘𝐴)↑2)))
3526, 34mpbird 248 . . . . . . . . . 10 (𝜑 → e ≤ (√‘𝐴))
363rpred 12073 . . . . . . . . . 10 (𝜑 → (√‘𝐵) ∈ ℝ)
37 bposlem7.6 . . . . . . . . . . . 12 (𝜑 → (e↑2) ≤ 𝐵)
382rprege0d 12080 . . . . . . . . . . . . 13 (𝜑 → (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵))
39 resqrtth 14284 . . . . . . . . . . . . 13 ((𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) → ((√‘𝐵)↑2) = 𝐵)
4038, 39syl 17 . . . . . . . . . . . 12 (𝜑 → ((√‘𝐵)↑2) = 𝐵)
4137, 40breqtrrd 4839 . . . . . . . . . . 11 (𝜑 → (e↑2) ≤ ((√‘𝐵)↑2))
423rpge0d 12077 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (√‘𝐵))
43 le2sq 13148 . . . . . . . . . . . . 13 (((e ∈ ℝ ∧ 0 ≤ e) ∧ ((√‘𝐵) ∈ ℝ ∧ 0 ≤ (√‘𝐵))) → (e ≤ (√‘𝐵) ↔ (e↑2) ≤ ((√‘𝐵)↑2)))
4428, 31, 43mpanl12 693 . . . . . . . . . . . 12 (((√‘𝐵) ∈ ℝ ∧ 0 ≤ (√‘𝐵)) → (e ≤ (√‘𝐵) ↔ (e↑2) ≤ ((√‘𝐵)↑2)))
4536, 42, 44syl2anc 579 . . . . . . . . . . 11 (𝜑 → (e ≤ (√‘𝐵) ↔ (e↑2) ≤ ((√‘𝐵)↑2)))
4641, 45mpbird 248 . . . . . . . . . 10 (𝜑 → e ≤ (√‘𝐵))
47 logdivlt 24661 . . . . . . . . . 10 ((((√‘𝐴) ∈ ℝ ∧ e ≤ (√‘𝐴)) ∧ ((√‘𝐵) ∈ ℝ ∧ e ≤ (√‘𝐵))) → ((√‘𝐴) < (√‘𝐵) ↔ ((log‘(√‘𝐵)) / (√‘𝐵)) < ((log‘(√‘𝐴)) / (√‘𝐴))))
4821, 35, 36, 46, 47syl22anc 867 . . . . . . . . 9 (𝜑 → ((√‘𝐴) < (√‘𝐵) ↔ ((log‘(√‘𝐵)) / (√‘𝐵)) < ((log‘(√‘𝐴)) / (√‘𝐴))))
4921, 36, 27, 42lt2sqd 13253 . . . . . . . . 9 (𝜑 → ((√‘𝐴) < (√‘𝐵) ↔ ((√‘𝐴)↑2) < ((√‘𝐵)↑2)))
5020, 48, 493bitr2rd 299 . . . . . . . 8 (𝜑 → (((√‘𝐴)↑2) < ((√‘𝐵)↑2) ↔ (𝐺‘(√‘𝐵)) < (𝐺‘(√‘𝐴))))
5125, 40breq12d 4824 . . . . . . . 8 (𝜑 → (((√‘𝐴)↑2) < ((√‘𝐵)↑2) ↔ 𝐴 < 𝐵))
52 relogcl 24616 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
53 rerpdivcl 12062 . . . . . . . . . . . . 13 (((log‘𝑥) ∈ ℝ ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥) / 𝑥) ∈ ℝ)
5452, 53mpancom 679 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+ → ((log‘𝑥) / 𝑥) ∈ ℝ)
557, 54fmpti 6574 . . . . . . . . . . 11 𝐺:ℝ+⟶ℝ
5655ffvelrni 6550 . . . . . . . . . 10 ((√‘𝐵) ∈ ℝ+ → (𝐺‘(√‘𝐵)) ∈ ℝ)
573, 56syl 17 . . . . . . . . 9 (𝜑 → (𝐺‘(√‘𝐵)) ∈ ℝ)
5855ffvelrni 6550 . . . . . . . . . 10 ((√‘𝐴) ∈ ℝ+ → (𝐺‘(√‘𝐴)) ∈ ℝ)
5913, 58syl 17 . . . . . . . . 9 (𝜑 → (𝐺‘(√‘𝐴)) ∈ ℝ)
60 2rp 12036 . . . . . . . . . 10 2 ∈ ℝ+
61 rpsqrtcl 14293 . . . . . . . . . 10 (2 ∈ ℝ+ → (√‘2) ∈ ℝ+)
6260, 61mp1i 13 . . . . . . . . 9 (𝜑 → (√‘2) ∈ ℝ+)
6357, 59, 62ltmul2d 12115 . . . . . . . 8 (𝜑 → ((𝐺‘(√‘𝐵)) < (𝐺‘(√‘𝐴)) ↔ ((√‘2) · (𝐺‘(√‘𝐵))) < ((√‘2) · (𝐺‘(√‘𝐴)))))
6450, 51, 633bitr3d 300 . . . . . . 7 (𝜑 → (𝐴 < 𝐵 ↔ ((√‘2) · (𝐺‘(√‘𝐵))) < ((√‘2) · (𝐺‘(√‘𝐴)))))
6564biimpd 220 . . . . . 6 (𝜑 → (𝐴 < 𝐵 → ((√‘2) · (𝐺‘(√‘𝐵))) < ((√‘2) · (𝐺‘(√‘𝐴)))))
6611nnred 11293 . . . . . . . . . 10 (𝜑𝐴 ∈ ℝ)
671nnred 11293 . . . . . . . . . 10 (𝜑𝐵 ∈ ℝ)
68 2re 11348 . . . . . . . . . . . 12 2 ∈ ℝ
69 2pos 11384 . . . . . . . . . . . 12 0 < 2
7068, 69pm3.2i 462 . . . . . . . . . . 11 (2 ∈ ℝ ∧ 0 < 2)
7170a1i 11 . . . . . . . . . 10 (𝜑 → (2 ∈ ℝ ∧ 0 < 2))
72 ltdiv1 11143 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝐴 < 𝐵 ↔ (𝐴 / 2) < (𝐵 / 2)))
7366, 67, 71, 72syl3anc 1490 . . . . . . . . 9 (𝜑 → (𝐴 < 𝐵 ↔ (𝐴 / 2) < (𝐵 / 2)))
7412rphalfcld 12085 . . . . . . . . . . 11 (𝜑 → (𝐴 / 2) ∈ ℝ+)
7574rpred 12073 . . . . . . . . . 10 (𝜑 → (𝐴 / 2) ∈ ℝ)
7628, 68remulcli 10312 . . . . . . . . . . . . 13 (e · 2) ∈ ℝ
7776a1i 11 . . . . . . . . . . . 12 (𝜑 → (e · 2) ∈ ℝ)
7828resqcli 13159 . . . . . . . . . . . . 13 (e↑2) ∈ ℝ
7978a1i 11 . . . . . . . . . . . 12 (𝜑 → (e↑2) ∈ ℝ)
80 egt2lt3 15219 . . . . . . . . . . . . . . . . 17 (2 < e ∧ e < 3)
8180simpli 476 . . . . . . . . . . . . . . . 16 2 < e
8268, 28, 81ltleii 10416 . . . . . . . . . . . . . . 15 2 ≤ e
8368, 28, 28lemul2i 11203 . . . . . . . . . . . . . . . 16 (0 < e → (2 ≤ e ↔ (e · 2) ≤ (e · e)))
8430, 83ax-mp 5 . . . . . . . . . . . . . . 15 (2 ≤ e ↔ (e · 2) ≤ (e · e))
8582, 84mpbi 221 . . . . . . . . . . . . . 14 (e · 2) ≤ (e · e)
8628recni 10310 . . . . . . . . . . . . . . 15 e ∈ ℂ
8786sqvali 13153 . . . . . . . . . . . . . 14 (e↑2) = (e · e)
8885, 87breqtrri 4838 . . . . . . . . . . . . 13 (e · 2) ≤ (e↑2)
8988a1i 11 . . . . . . . . . . . 12 (𝜑 → (e · 2) ≤ (e↑2))
9077, 79, 66, 89, 22letrd 10450 . . . . . . . . . . 11 (𝜑 → (e · 2) ≤ 𝐴)
91 lemuldiv 11159 . . . . . . . . . . . . 13 ((e ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((e · 2) ≤ 𝐴 ↔ e ≤ (𝐴 / 2)))
9228, 70, 91mp3an13 1576 . . . . . . . . . . . 12 (𝐴 ∈ ℝ → ((e · 2) ≤ 𝐴 ↔ e ≤ (𝐴 / 2)))
9366, 92syl 17 . . . . . . . . . . 11 (𝜑 → ((e · 2) ≤ 𝐴 ↔ e ≤ (𝐴 / 2)))
9490, 93mpbid 223 . . . . . . . . . 10 (𝜑 → e ≤ (𝐴 / 2))
952rphalfcld 12085 . . . . . . . . . . 11 (𝜑 → (𝐵 / 2) ∈ ℝ+)
9695rpred 12073 . . . . . . . . . 10 (𝜑 → (𝐵 / 2) ∈ ℝ)
9777, 79, 67, 89, 37letrd 10450 . . . . . . . . . . 11 (𝜑 → (e · 2) ≤ 𝐵)
98 lemuldiv 11159 . . . . . . . . . . . . 13 ((e ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((e · 2) ≤ 𝐵 ↔ e ≤ (𝐵 / 2)))
9928, 70, 98mp3an13 1576 . . . . . . . . . . . 12 (𝐵 ∈ ℝ → ((e · 2) ≤ 𝐵 ↔ e ≤ (𝐵 / 2)))
10067, 99syl 17 . . . . . . . . . . 11 (𝜑 → ((e · 2) ≤ 𝐵 ↔ e ≤ (𝐵 / 2)))
10197, 100mpbid 223 . . . . . . . . . 10 (𝜑 → e ≤ (𝐵 / 2))
102 logdivlt 24661 . . . . . . . . . 10 ((((𝐴 / 2) ∈ ℝ ∧ e ≤ (𝐴 / 2)) ∧ ((𝐵 / 2) ∈ ℝ ∧ e ≤ (𝐵 / 2))) → ((𝐴 / 2) < (𝐵 / 2) ↔ ((log‘(𝐵 / 2)) / (𝐵 / 2)) < ((log‘(𝐴 / 2)) / (𝐴 / 2))))
10375, 94, 96, 101, 102syl22anc 867 . . . . . . . . 9 (𝜑 → ((𝐴 / 2) < (𝐵 / 2) ↔ ((log‘(𝐵 / 2)) / (𝐵 / 2)) < ((log‘(𝐴 / 2)) / (𝐴 / 2))))
10473, 103bitrd 270 . . . . . . . 8 (𝜑 → (𝐴 < 𝐵 ↔ ((log‘(𝐵 / 2)) / (𝐵 / 2)) < ((log‘(𝐴 / 2)) / (𝐴 / 2))))
105 fveq2 6377 . . . . . . . . . . . 12 (𝑥 = (𝐵 / 2) → (log‘𝑥) = (log‘(𝐵 / 2)))
106 id 22 . . . . . . . . . . . 12 (𝑥 = (𝐵 / 2) → 𝑥 = (𝐵 / 2))
107105, 106oveq12d 6862 . . . . . . . . . . 11 (𝑥 = (𝐵 / 2) → ((log‘𝑥) / 𝑥) = ((log‘(𝐵 / 2)) / (𝐵 / 2)))
108 ovex 6876 . . . . . . . . . . 11 ((log‘(𝐵 / 2)) / (𝐵 / 2)) ∈ V
109107, 7, 108fvmpt 6473 . . . . . . . . . 10 ((𝐵 / 2) ∈ ℝ+ → (𝐺‘(𝐵 / 2)) = ((log‘(𝐵 / 2)) / (𝐵 / 2)))
11095, 109syl 17 . . . . . . . . 9 (𝜑 → (𝐺‘(𝐵 / 2)) = ((log‘(𝐵 / 2)) / (𝐵 / 2)))
111 fveq2 6377 . . . . . . . . . . . 12 (𝑥 = (𝐴 / 2) → (log‘𝑥) = (log‘(𝐴 / 2)))
112 id 22 . . . . . . . . . . . 12 (𝑥 = (𝐴 / 2) → 𝑥 = (𝐴 / 2))
113111, 112oveq12d 6862 . . . . . . . . . . 11 (𝑥 = (𝐴 / 2) → ((log‘𝑥) / 𝑥) = ((log‘(𝐴 / 2)) / (𝐴 / 2)))
114 ovex 6876 . . . . . . . . . . 11 ((log‘(𝐴 / 2)) / (𝐴 / 2)) ∈ V
115113, 7, 114fvmpt 6473 . . . . . . . . . 10 ((𝐴 / 2) ∈ ℝ+ → (𝐺‘(𝐴 / 2)) = ((log‘(𝐴 / 2)) / (𝐴 / 2)))
11674, 115syl 17 . . . . . . . . 9 (𝜑 → (𝐺‘(𝐴 / 2)) = ((log‘(𝐴 / 2)) / (𝐴 / 2)))
117110, 116breq12d 4824 . . . . . . . 8 (𝜑 → ((𝐺‘(𝐵 / 2)) < (𝐺‘(𝐴 / 2)) ↔ ((log‘(𝐵 / 2)) / (𝐵 / 2)) < ((log‘(𝐴 / 2)) / (𝐴 / 2))))
11855ffvelrni 6550 . . . . . . . . . 10 ((𝐵 / 2) ∈ ℝ+ → (𝐺‘(𝐵 / 2)) ∈ ℝ)
11995, 118syl 17 . . . . . . . . 9 (𝜑 → (𝐺‘(𝐵 / 2)) ∈ ℝ)
12055ffvelrni 6550 . . . . . . . . . 10 ((𝐴 / 2) ∈ ℝ+ → (𝐺‘(𝐴 / 2)) ∈ ℝ)
12174, 120syl 17 . . . . . . . . 9 (𝜑 → (𝐺‘(𝐴 / 2)) ∈ ℝ)
122 9nn 11378 . . . . . . . . . . 11 9 ∈ ℕ
123 4nn 11358 . . . . . . . . . . 11 4 ∈ ℕ
124 nnrp 12044 . . . . . . . . . . . 12 (9 ∈ ℕ → 9 ∈ ℝ+)
125 nnrp 12044 . . . . . . . . . . . 12 (4 ∈ ℕ → 4 ∈ ℝ+)
126 rpdivcl 12057 . . . . . . . . . . . 12 ((9 ∈ ℝ+ ∧ 4 ∈ ℝ+) → (9 / 4) ∈ ℝ+)
127124, 125, 126syl2an 589 . . . . . . . . . . 11 ((9 ∈ ℕ ∧ 4 ∈ ℕ) → (9 / 4) ∈ ℝ+)
128122, 123, 127mp2an 683 . . . . . . . . . 10 (9 / 4) ∈ ℝ+
129128a1i 11 . . . . . . . . 9 (𝜑 → (9 / 4) ∈ ℝ+)
130119, 121, 129ltmul2d 12115 . . . . . . . 8 (𝜑 → ((𝐺‘(𝐵 / 2)) < (𝐺‘(𝐴 / 2)) ↔ ((9 / 4) · (𝐺‘(𝐵 / 2))) < ((9 / 4) · (𝐺‘(𝐴 / 2)))))
131104, 117, 1303bitr2d 298 . . . . . . 7 (𝜑 → (𝐴 < 𝐵 ↔ ((9 / 4) · (𝐺‘(𝐵 / 2))) < ((9 / 4) · (𝐺‘(𝐴 / 2)))))
132131biimpd 220 . . . . . 6 (𝜑 → (𝐴 < 𝐵 → ((9 / 4) · (𝐺‘(𝐵 / 2))) < ((9 / 4) · (𝐺‘(𝐴 / 2)))))
13365, 132jcad 508 . . . . 5 (𝜑 → (𝐴 < 𝐵 → (((√‘2) · (𝐺‘(√‘𝐵))) < ((√‘2) · (𝐺‘(√‘𝐴))) ∧ ((9 / 4) · (𝐺‘(𝐵 / 2))) < ((9 / 4) · (𝐺‘(𝐴 / 2))))))
134 sqrt2re 15265 . . . . . . 7 (√‘2) ∈ ℝ
135 remulcl 10276 . . . . . . 7 (((√‘2) ∈ ℝ ∧ (𝐺‘(√‘𝐵)) ∈ ℝ) → ((√‘2) · (𝐺‘(√‘𝐵))) ∈ ℝ)
136134, 57, 135sylancr 581 . . . . . 6 (𝜑 → ((√‘2) · (𝐺‘(√‘𝐵))) ∈ ℝ)
137 9re 11379 . . . . . . . 8 9 ∈ ℝ
138 4re 11359 . . . . . . . 8 4 ∈ ℝ
139 4ne0 11389 . . . . . . . 8 4 ≠ 0
140137, 138, 139redivcli 11048 . . . . . . 7 (9 / 4) ∈ ℝ
141 remulcl 10276 . . . . . . 7 (((9 / 4) ∈ ℝ ∧ (𝐺‘(𝐵 / 2)) ∈ ℝ) → ((9 / 4) · (𝐺‘(𝐵 / 2))) ∈ ℝ)
142140, 119, 141sylancr 581 . . . . . 6 (𝜑 → ((9 / 4) · (𝐺‘(𝐵 / 2))) ∈ ℝ)
143 remulcl 10276 . . . . . . 7 (((√‘2) ∈ ℝ ∧ (𝐺‘(√‘𝐴)) ∈ ℝ) → ((√‘2) · (𝐺‘(√‘𝐴))) ∈ ℝ)
144134, 59, 143sylancr 581 . . . . . 6 (𝜑 → ((√‘2) · (𝐺‘(√‘𝐴))) ∈ ℝ)
145 remulcl 10276 . . . . . . 7 (((9 / 4) ∈ ℝ ∧ (𝐺‘(𝐴 / 2)) ∈ ℝ) → ((9 / 4) · (𝐺‘(𝐴 / 2))) ∈ ℝ)
146140, 121, 145sylancr 581 . . . . . 6 (𝜑 → ((9 / 4) · (𝐺‘(𝐴 / 2))) ∈ ℝ)
147 lt2add 10769 . . . . . 6 (((((√‘2) · (𝐺‘(√‘𝐵))) ∈ ℝ ∧ ((9 / 4) · (𝐺‘(𝐵 / 2))) ∈ ℝ) ∧ (((√‘2) · (𝐺‘(√‘𝐴))) ∈ ℝ ∧ ((9 / 4) · (𝐺‘(𝐴 / 2))) ∈ ℝ)) → ((((√‘2) · (𝐺‘(√‘𝐵))) < ((√‘2) · (𝐺‘(√‘𝐴))) ∧ ((9 / 4) · (𝐺‘(𝐵 / 2))) < ((9 / 4) · (𝐺‘(𝐴 / 2)))) → (((√‘2) · (𝐺‘(√‘𝐵))) + ((9 / 4) · (𝐺‘(𝐵 / 2)))) < (((√‘2) · (𝐺‘(√‘𝐴))) + ((9 / 4) · (𝐺‘(𝐴 / 2))))))
148136, 142, 144, 146, 147syl22anc 867 . . . . 5 (𝜑 → ((((√‘2) · (𝐺‘(√‘𝐵))) < ((√‘2) · (𝐺‘(√‘𝐴))) ∧ ((9 / 4) · (𝐺‘(𝐵 / 2))) < ((9 / 4) · (𝐺‘(𝐴 / 2)))) → (((√‘2) · (𝐺‘(√‘𝐵))) + ((9 / 4) · (𝐺‘(𝐵 / 2)))) < (((√‘2) · (𝐺‘(√‘𝐴))) + ((9 / 4) · (𝐺‘(𝐴 / 2))))))
149133, 148syld 47 . . . 4 (𝜑 → (𝐴 < 𝐵 → (((√‘2) · (𝐺‘(√‘𝐵))) + ((9 / 4) · (𝐺‘(𝐵 / 2)))) < (((√‘2) · (𝐺‘(√‘𝐴))) + ((9 / 4) · (𝐺‘(𝐴 / 2))))))
150 ltmul2 11130 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝐴 < 𝐵 ↔ (2 · 𝐴) < (2 · 𝐵)))
15166, 67, 71, 150syl3anc 1490 . . . . . 6 (𝜑 → (𝐴 < 𝐵 ↔ (2 · 𝐴) < (2 · 𝐵)))
152 rpmulcl 12056 . . . . . . . . . 10 ((2 ∈ ℝ+𝐴 ∈ ℝ+) → (2 · 𝐴) ∈ ℝ+)
15360, 12, 152sylancr 581 . . . . . . . . 9 (𝜑 → (2 · 𝐴) ∈ ℝ+)
154153rpsqrtcld 14438 . . . . . . . 8 (𝜑 → (√‘(2 · 𝐴)) ∈ ℝ+)
155 rpmulcl 12056 . . . . . . . . . 10 ((2 ∈ ℝ+𝐵 ∈ ℝ+) → (2 · 𝐵) ∈ ℝ+)
15660, 2, 155sylancr 581 . . . . . . . . 9 (𝜑 → (2 · 𝐵) ∈ ℝ+)
157156rpsqrtcld 14438 . . . . . . . 8 (𝜑 → (√‘(2 · 𝐵)) ∈ ℝ+)
158 rprege0 12048 . . . . . . . . 9 ((√‘(2 · 𝐴)) ∈ ℝ+ → ((√‘(2 · 𝐴)) ∈ ℝ ∧ 0 ≤ (√‘(2 · 𝐴))))
159 rprege0 12048 . . . . . . . . 9 ((√‘(2 · 𝐵)) ∈ ℝ+ → ((√‘(2 · 𝐵)) ∈ ℝ ∧ 0 ≤ (√‘(2 · 𝐵))))
160 lt2sq 13147 . . . . . . . . 9 ((((√‘(2 · 𝐴)) ∈ ℝ ∧ 0 ≤ (√‘(2 · 𝐴))) ∧ ((√‘(2 · 𝐵)) ∈ ℝ ∧ 0 ≤ (√‘(2 · 𝐵)))) → ((√‘(2 · 𝐴)) < (√‘(2 · 𝐵)) ↔ ((√‘(2 · 𝐴))↑2) < ((√‘(2 · 𝐵))↑2)))
161158, 159, 160syl2an 589 . . . . . . . 8 (((√‘(2 · 𝐴)) ∈ ℝ+ ∧ (√‘(2 · 𝐵)) ∈ ℝ+) → ((√‘(2 · 𝐴)) < (√‘(2 · 𝐵)) ↔ ((√‘(2 · 𝐴))↑2) < ((√‘(2 · 𝐵))↑2)))
162154, 157, 161syl2anc 579 . . . . . . 7 (𝜑 → ((√‘(2 · 𝐴)) < (√‘(2 · 𝐵)) ↔ ((√‘(2 · 𝐴))↑2) < ((√‘(2 · 𝐵))↑2)))
163153rprege0d 12080 . . . . . . . . 9 (𝜑 → ((2 · 𝐴) ∈ ℝ ∧ 0 ≤ (2 · 𝐴)))
164 resqrtth 14284 . . . . . . . . 9 (((2 · 𝐴) ∈ ℝ ∧ 0 ≤ (2 · 𝐴)) → ((√‘(2 · 𝐴))↑2) = (2 · 𝐴))
165163, 164syl 17 . . . . . . . 8 (𝜑 → ((√‘(2 · 𝐴))↑2) = (2 · 𝐴))
166156rprege0d 12080 . . . . . . . . 9 (𝜑 → ((2 · 𝐵) ∈ ℝ ∧ 0 ≤ (2 · 𝐵)))
167 resqrtth 14284 . . . . . . . . 9 (((2 · 𝐵) ∈ ℝ ∧ 0 ≤ (2 · 𝐵)) → ((√‘(2 · 𝐵))↑2) = (2 · 𝐵))
168166, 167syl 17 . . . . . . . 8 (𝜑 → ((√‘(2 · 𝐵))↑2) = (2 · 𝐵))
169165, 168breq12d 4824 . . . . . . 7 (𝜑 → (((√‘(2 · 𝐴))↑2) < ((√‘(2 · 𝐵))↑2) ↔ (2 · 𝐴) < (2 · 𝐵)))
170162, 169bitr2d 271 . . . . . 6 (𝜑 → ((2 · 𝐴) < (2 · 𝐵) ↔ (√‘(2 · 𝐴)) < (√‘(2 · 𝐵))))
171 1lt2 11451 . . . . . . . . 9 1 < 2
172 rplogcl 24644 . . . . . . . . 9 ((2 ∈ ℝ ∧ 1 < 2) → (log‘2) ∈ ℝ+)
17368, 171, 172mp2an 683 . . . . . . . 8 (log‘2) ∈ ℝ+
174173a1i 11 . . . . . . 7 (𝜑 → (log‘2) ∈ ℝ+)
175154, 157, 174ltdiv2d 12096 . . . . . 6 (𝜑 → ((√‘(2 · 𝐴)) < (√‘(2 · 𝐵)) ↔ ((log‘2) / (√‘(2 · 𝐵))) < ((log‘2) / (√‘(2 · 𝐴)))))
176151, 170, 1753bitrd 296 . . . . 5 (𝜑 → (𝐴 < 𝐵 ↔ ((log‘2) / (√‘(2 · 𝐵))) < ((log‘2) / (√‘(2 · 𝐴)))))
177176biimpd 220 . . . 4 (𝜑 → (𝐴 < 𝐵 → ((log‘2) / (√‘(2 · 𝐵))) < ((log‘2) / (√‘(2 · 𝐴)))))
178149, 177jcad 508 . . 3 (𝜑 → (𝐴 < 𝐵 → ((((√‘2) · (𝐺‘(√‘𝐵))) + ((9 / 4) · (𝐺‘(𝐵 / 2)))) < (((√‘2) · (𝐺‘(√‘𝐴))) + ((9 / 4) · (𝐺‘(𝐴 / 2)))) ∧ ((log‘2) / (√‘(2 · 𝐵))) < ((log‘2) / (√‘(2 · 𝐴))))))
179136, 142readdcld 10325 . . . 4 (𝜑 → (((√‘2) · (𝐺‘(√‘𝐵))) + ((9 / 4) · (𝐺‘(𝐵 / 2)))) ∈ ℝ)
180 rpre 12039 . . . . . 6 ((log‘2) ∈ ℝ+ → (log‘2) ∈ ℝ)
181173, 180ax-mp 5 . . . . 5 (log‘2) ∈ ℝ
182 rerpdivcl 12062 . . . . 5 (((log‘2) ∈ ℝ ∧ (√‘(2 · 𝐵)) ∈ ℝ+) → ((log‘2) / (√‘(2 · 𝐵))) ∈ ℝ)
183181, 157, 182sylancr 581 . . . 4 (𝜑 → ((log‘2) / (√‘(2 · 𝐵))) ∈ ℝ)
184144, 146readdcld 10325 . . . 4 (𝜑 → (((√‘2) · (𝐺‘(√‘𝐴))) + ((9 / 4) · (𝐺‘(𝐴 / 2)))) ∈ ℝ)
185 rerpdivcl 12062 . . . . 5 (((log‘2) ∈ ℝ ∧ (√‘(2 · 𝐴)) ∈ ℝ+) → ((log‘2) / (√‘(2 · 𝐴))) ∈ ℝ)
186181, 154, 185sylancr 581 . . . 4 (𝜑 → ((log‘2) / (√‘(2 · 𝐴))) ∈ ℝ)
187 lt2add 10769 . . . 4 ((((((√‘2) · (𝐺‘(√‘𝐵))) + ((9 / 4) · (𝐺‘(𝐵 / 2)))) ∈ ℝ ∧ ((log‘2) / (√‘(2 · 𝐵))) ∈ ℝ) ∧ ((((√‘2) · (𝐺‘(√‘𝐴))) + ((9 / 4) · (𝐺‘(𝐴 / 2)))) ∈ ℝ ∧ ((log‘2) / (√‘(2 · 𝐴))) ∈ ℝ)) → (((((√‘2) · (𝐺‘(√‘𝐵))) + ((9 / 4) · (𝐺‘(𝐵 / 2)))) < (((√‘2) · (𝐺‘(√‘𝐴))) + ((9 / 4) · (𝐺‘(𝐴 / 2)))) ∧ ((log‘2) / (√‘(2 · 𝐵))) < ((log‘2) / (√‘(2 · 𝐴)))) → ((((√‘2) · (𝐺‘(√‘𝐵))) + ((9 / 4) · (𝐺‘(𝐵 / 2)))) + ((log‘2) / (√‘(2 · 𝐵)))) < ((((√‘2) · (𝐺‘(√‘𝐴))) + ((9 / 4) · (𝐺‘(𝐴 / 2)))) + ((log‘2) / (√‘(2 · 𝐴))))))
188179, 183, 184, 186, 187syl22anc 867 . . 3 (𝜑 → (((((√‘2) · (𝐺‘(√‘𝐵))) + ((9 / 4) · (𝐺‘(𝐵 / 2)))) < (((√‘2) · (𝐺‘(√‘𝐴))) + ((9 / 4) · (𝐺‘(𝐴 / 2)))) ∧ ((log‘2) / (√‘(2 · 𝐵))) < ((log‘2) / (√‘(2 · 𝐴)))) → ((((√‘2) · (𝐺‘(√‘𝐵))) + ((9 / 4) · (𝐺‘(𝐵 / 2)))) + ((log‘2) / (√‘(2 · 𝐵)))) < ((((√‘2) · (𝐺‘(√‘𝐴))) + ((9 / 4) · (𝐺‘(𝐴 / 2)))) + ((log‘2) / (√‘(2 · 𝐴))))))
189178, 188syld 47 . 2 (𝜑 → (𝐴 < 𝐵 → ((((√‘2) · (𝐺‘(√‘𝐵))) + ((9 / 4) · (𝐺‘(𝐵 / 2)))) + ((log‘2) / (√‘(2 · 𝐵)))) < ((((√‘2) · (𝐺‘(√‘𝐴))) + ((9 / 4) · (𝐺‘(𝐴 / 2)))) + ((log‘2) / (√‘(2 · 𝐴))))))
190 2fveq3 6382 . . . . . . . 8 (𝑛 = 𝐵 → (𝐺‘(√‘𝑛)) = (𝐺‘(√‘𝐵)))
191190oveq2d 6860 . . . . . . 7 (𝑛 = 𝐵 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2) · (𝐺‘(√‘𝐵))))
192 fvoveq1 6867 . . . . . . . 8 (𝑛 = 𝐵 → (𝐺‘(𝑛 / 2)) = (𝐺‘(𝐵 / 2)))
193192oveq2d 6860 . . . . . . 7 (𝑛 = 𝐵 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · (𝐺‘(𝐵 / 2))))
194191, 193oveq12d 6862 . . . . . 6 (𝑛 = 𝐵 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = (((√‘2) · (𝐺‘(√‘𝐵))) + ((9 / 4) · (𝐺‘(𝐵 / 2)))))
195 oveq2 6852 . . . . . . . 8 (𝑛 = 𝐵 → (2 · 𝑛) = (2 · 𝐵))
196195fveq2d 6381 . . . . . . 7 (𝑛 = 𝐵 → (√‘(2 · 𝑛)) = (√‘(2 · 𝐵)))
197196oveq2d 6860 . . . . . 6 (𝑛 = 𝐵 → ((log‘2) / (√‘(2 · 𝑛))) = ((log‘2) / (√‘(2 · 𝐵))))
198194, 197oveq12d 6862 . . . . 5 (𝑛 = 𝐵 → ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))) = ((((√‘2) · (𝐺‘(√‘𝐵))) + ((9 / 4) · (𝐺‘(𝐵 / 2)))) + ((log‘2) / (√‘(2 · 𝐵)))))
199 bposlem7.1 . . . . 5 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))
200 ovex 6876 . . . . 5 ((((√‘2) · (𝐺‘(√‘𝐵))) + ((9 / 4) · (𝐺‘(𝐵 / 2)))) + ((log‘2) / (√‘(2 · 𝐵)))) ∈ V
201198, 199, 200fvmpt 6473 . . . 4 (𝐵 ∈ ℕ → (𝐹𝐵) = ((((√‘2) · (𝐺‘(√‘𝐵))) + ((9 / 4) · (𝐺‘(𝐵 / 2)))) + ((log‘2) / (√‘(2 · 𝐵)))))
2021, 201syl 17 . . 3 (𝜑 → (𝐹𝐵) = ((((√‘2) · (𝐺‘(√‘𝐵))) + ((9 / 4) · (𝐺‘(𝐵 / 2)))) + ((log‘2) / (√‘(2 · 𝐵)))))
203 2fveq3 6382 . . . . . . . 8 (𝑛 = 𝐴 → (𝐺‘(√‘𝑛)) = (𝐺‘(√‘𝐴)))
204203oveq2d 6860 . . . . . . 7 (𝑛 = 𝐴 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2) · (𝐺‘(√‘𝐴))))
205 fvoveq1 6867 . . . . . . . 8 (𝑛 = 𝐴 → (𝐺‘(𝑛 / 2)) = (𝐺‘(𝐴 / 2)))
206205oveq2d 6860 . . . . . . 7 (𝑛 = 𝐴 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · (𝐺‘(𝐴 / 2))))
207204, 206oveq12d 6862 . . . . . 6 (𝑛 = 𝐴 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = (((√‘2) · (𝐺‘(√‘𝐴))) + ((9 / 4) · (𝐺‘(𝐴 / 2)))))
208 oveq2 6852 . . . . . . . 8 (𝑛 = 𝐴 → (2 · 𝑛) = (2 · 𝐴))
209208fveq2d 6381 . . . . . . 7 (𝑛 = 𝐴 → (√‘(2 · 𝑛)) = (√‘(2 · 𝐴)))
210209oveq2d 6860 . . . . . 6 (𝑛 = 𝐴 → ((log‘2) / (√‘(2 · 𝑛))) = ((log‘2) / (√‘(2 · 𝐴))))
211207, 210oveq12d 6862 . . . . 5 (𝑛 = 𝐴 → ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))) = ((((√‘2) · (𝐺‘(√‘𝐴))) + ((9 / 4) · (𝐺‘(𝐴 / 2)))) + ((log‘2) / (√‘(2 · 𝐴)))))
212 ovex 6876 . . . . 5 ((((√‘2) · (𝐺‘(√‘𝐴))) + ((9 / 4) · (𝐺‘(𝐴 / 2)))) + ((log‘2) / (√‘(2 · 𝐴)))) ∈ V
213211, 199, 212fvmpt 6473 . . . 4 (𝐴 ∈ ℕ → (𝐹𝐴) = ((((√‘2) · (𝐺‘(√‘𝐴))) + ((9 / 4) · (𝐺‘(𝐴 / 2)))) + ((log‘2) / (√‘(2 · 𝐴)))))
21411, 213syl 17 . . 3 (𝜑 → (𝐹𝐴) = ((((√‘2) · (𝐺‘(√‘𝐴))) + ((9 / 4) · (𝐺‘(𝐴 / 2)))) + ((log‘2) / (√‘(2 · 𝐴)))))
215202, 214breq12d 4824 . 2 (𝜑 → ((𝐹𝐵) < (𝐹𝐴) ↔ ((((√‘2) · (𝐺‘(√‘𝐵))) + ((9 / 4) · (𝐺‘(𝐵 / 2)))) + ((log‘2) / (√‘(2 · 𝐵)))) < ((((√‘2) · (𝐺‘(√‘𝐴))) + ((9 / 4) · (𝐺‘(𝐴 / 2)))) + ((log‘2) / (√‘(2 · 𝐴))))))
216189, 215sylibrd 250 1 (𝜑 → (𝐴 < 𝐵 → (𝐹𝐵) < (𝐹𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155   class class class wbr 4811  cmpt 4890  cfv 6070  (class class class)co 6844  cr 10190  0cc0 10191  1c1 10192   + caddc 10194   · cmul 10196   < clt 10330  cle 10331   / cdiv 10940  cn 11276  2c2 11329  3c3 11330  4c4 11331  9c9 11336  +crp 12031  cexp 13070  csqrt 14261  eceu 15078  logclog 24595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149  ax-inf2 8755  ax-cnex 10247  ax-resscn 10248  ax-1cn 10249  ax-icn 10250  ax-addcl 10251  ax-addrcl 10252  ax-mulcl 10253  ax-mulrcl 10254  ax-mulcom 10255  ax-addass 10256  ax-mulass 10257  ax-distr 10258  ax-i2m1 10259  ax-1ne0 10260  ax-1rid 10261  ax-rnegex 10262  ax-rrecex 10263  ax-cnre 10264  ax-pre-lttri 10265  ax-pre-lttrn 10266  ax-pre-ltadd 10267  ax-pre-mulgt0 10268  ax-pre-sup 10269  ax-addf 10270  ax-mulf 10271
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-iin 4681  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-se 5239  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-isom 6079  df-riota 6805  df-ov 6847  df-oprab 6848  df-mpt2 6849  df-of 7097  df-om 7266  df-1st 7368  df-2nd 7369  df-supp 7500  df-wrecs 7612  df-recs 7674  df-rdg 7712  df-1o 7766  df-2o 7767  df-oadd 7770  df-er 7949  df-map 8064  df-pm 8065  df-ixp 8116  df-en 8163  df-dom 8164  df-sdom 8165  df-fin 8166  df-fsupp 8485  df-fi 8526  df-sup 8557  df-inf 8558  df-oi 8624  df-card 9018  df-cda 9245  df-pnf 10332  df-mnf 10333  df-xr 10334  df-ltxr 10335  df-le 10336  df-sub 10524  df-neg 10525  df-div 10941  df-nn 11277  df-2 11337  df-3 11338  df-4 11339  df-5 11340  df-6 11341  df-7 11342  df-8 11343  df-9 11344  df-n0 11541  df-z 11627  df-dec 11744  df-uz 11890  df-q 11993  df-rp 12032  df-xneg 12149  df-xadd 12150  df-xmul 12151  df-ioo 12384  df-ioc 12385  df-ico 12386  df-icc 12387  df-fz 12537  df-fzo 12677  df-fl 12804  df-mod 12880  df-seq 13012  df-exp 13071  df-fac 13268  df-bc 13297  df-hash 13325  df-shft 14095  df-cj 14127  df-re 14128  df-im 14129  df-sqrt 14263  df-abs 14264  df-limsup 14490  df-clim 14507  df-rlim 14508  df-sum 14705  df-ef 15083  df-e 15084  df-sin 15085  df-cos 15086  df-pi 15088  df-struct 16135  df-ndx 16136  df-slot 16137  df-base 16139  df-sets 16140  df-ress 16141  df-plusg 16230  df-mulr 16231  df-starv 16232  df-sca 16233  df-vsca 16234  df-ip 16235  df-tset 16236  df-ple 16237  df-ds 16239  df-unif 16240  df-hom 16241  df-cco 16242  df-rest 16352  df-topn 16353  df-0g 16371  df-gsum 16372  df-topgen 16373  df-pt 16374  df-prds 16377  df-xrs 16431  df-qtop 16436  df-imas 16437  df-xps 16439  df-mre 16515  df-mrc 16516  df-acs 16518  df-mgm 17511  df-sgrp 17553  df-mnd 17564  df-submnd 17605  df-mulg 17811  df-cntz 18016  df-cmn 18464  df-psmet 20014  df-xmet 20015  df-met 20016  df-bl 20017  df-mopn 20018  df-fbas 20019  df-fg 20020  df-cnfld 20023  df-top 20981  df-topon 20998  df-topsp 21020  df-bases 21033  df-cld 21106  df-ntr 21107  df-cls 21108  df-nei 21185  df-lp 21223  df-perf 21224  df-cn 21314  df-cnp 21315  df-haus 21402  df-tx 21648  df-hmeo 21841  df-fil 21932  df-fm 22024  df-flim 22025  df-flf 22026  df-xms 22407  df-ms 22408  df-tms 22409  df-cncf 22963  df-limc 23924  df-dv 23925  df-log 24597
This theorem is referenced by:  bposlem9  25311
  Copyright terms: Public domain W3C validator