Step | Hyp | Ref
| Expression |
1 | | eluznn 11758 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈
(ℤ≥‘𝐴)) → 𝐵 ∈ ℕ) |
2 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑎 = 𝐵 → (!‘𝑎) = (!‘𝐵)) |
3 | 2 | negeqd 10275 |
. . . . . . 7
⊢ (𝑎 = 𝐵 → -(!‘𝑎) = -(!‘𝐵)) |
4 | 3 | oveq2d 6666 |
. . . . . 6
⊢ (𝑎 = 𝐵 → (2↑-(!‘𝑎)) = (2↑-(!‘𝐵))) |
5 | | aaliou3lem.b |
. . . . . 6
⊢ 𝐹 = (𝑎 ∈ ℕ ↦
(2↑-(!‘𝑎))) |
6 | | ovex 6678 |
. . . . . 6
⊢
(2↑-(!‘𝐵)) ∈ V |
7 | 4, 5, 6 | fvmpt 6282 |
. . . . 5
⊢ (𝐵 ∈ ℕ → (𝐹‘𝐵) = (2↑-(!‘𝐵))) |
8 | 1, 7 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝐵) = (2↑-(!‘𝐵))) |
9 | | 2rp 11837 |
. . . . 5
⊢ 2 ∈
ℝ+ |
10 | 1 | nnnn0d 11351 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈
(ℤ≥‘𝐴)) → 𝐵 ∈
ℕ0) |
11 | | faccl 13070 |
. . . . . . . 8
⊢ (𝐵 ∈ ℕ0
→ (!‘𝐵) ∈
ℕ) |
12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈
(ℤ≥‘𝐴)) → (!‘𝐵) ∈ ℕ) |
13 | 12 | nnzd 11481 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈
(ℤ≥‘𝐴)) → (!‘𝐵) ∈ ℤ) |
14 | 13 | znegcld 11484 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈
(ℤ≥‘𝐴)) → -(!‘𝐵) ∈ ℤ) |
15 | | rpexpcl 12879 |
. . . . 5
⊢ ((2
∈ ℝ+ ∧ -(!‘𝐵) ∈ ℤ) →
(2↑-(!‘𝐵))
∈ ℝ+) |
16 | 9, 14, 15 | sylancr 695 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈
(ℤ≥‘𝐴)) → (2↑-(!‘𝐵)) ∈
ℝ+) |
17 | 8, 16 | eqeltrd 2701 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝐵) ∈
ℝ+) |
18 | 17 | rpred 11872 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝐵) ∈ ℝ) |
19 | 17 | rpgt0d 11875 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈
(ℤ≥‘𝐴)) → 0 < (𝐹‘𝐵)) |
20 | | fveq2 6191 |
. . . . . 6
⊢ (𝑏 = 𝐴 → (𝐹‘𝑏) = (𝐹‘𝐴)) |
21 | | fveq2 6191 |
. . . . . 6
⊢ (𝑏 = 𝐴 → (𝐺‘𝑏) = (𝐺‘𝐴)) |
22 | 20, 21 | breq12d 4666 |
. . . . 5
⊢ (𝑏 = 𝐴 → ((𝐹‘𝑏) ≤ (𝐺‘𝑏) ↔ (𝐹‘𝐴) ≤ (𝐺‘𝐴))) |
23 | 22 | imbi2d 330 |
. . . 4
⊢ (𝑏 = 𝐴 → ((𝐴 ∈ ℕ → (𝐹‘𝑏) ≤ (𝐺‘𝑏)) ↔ (𝐴 ∈ ℕ → (𝐹‘𝐴) ≤ (𝐺‘𝐴)))) |
24 | | fveq2 6191 |
. . . . . 6
⊢ (𝑏 = 𝑑 → (𝐹‘𝑏) = (𝐹‘𝑑)) |
25 | | fveq2 6191 |
. . . . . 6
⊢ (𝑏 = 𝑑 → (𝐺‘𝑏) = (𝐺‘𝑑)) |
26 | 24, 25 | breq12d 4666 |
. . . . 5
⊢ (𝑏 = 𝑑 → ((𝐹‘𝑏) ≤ (𝐺‘𝑏) ↔ (𝐹‘𝑑) ≤ (𝐺‘𝑑))) |
27 | 26 | imbi2d 330 |
. . . 4
⊢ (𝑏 = 𝑑 → ((𝐴 ∈ ℕ → (𝐹‘𝑏) ≤ (𝐺‘𝑏)) ↔ (𝐴 ∈ ℕ → (𝐹‘𝑑) ≤ (𝐺‘𝑑)))) |
28 | | fveq2 6191 |
. . . . . 6
⊢ (𝑏 = (𝑑 + 1) → (𝐹‘𝑏) = (𝐹‘(𝑑 + 1))) |
29 | | fveq2 6191 |
. . . . . 6
⊢ (𝑏 = (𝑑 + 1) → (𝐺‘𝑏) = (𝐺‘(𝑑 + 1))) |
30 | 28, 29 | breq12d 4666 |
. . . . 5
⊢ (𝑏 = (𝑑 + 1) → ((𝐹‘𝑏) ≤ (𝐺‘𝑏) ↔ (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1)))) |
31 | 30 | imbi2d 330 |
. . . 4
⊢ (𝑏 = (𝑑 + 1) → ((𝐴 ∈ ℕ → (𝐹‘𝑏) ≤ (𝐺‘𝑏)) ↔ (𝐴 ∈ ℕ → (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1))))) |
32 | | fveq2 6191 |
. . . . . 6
⊢ (𝑏 = 𝐵 → (𝐹‘𝑏) = (𝐹‘𝐵)) |
33 | | fveq2 6191 |
. . . . . 6
⊢ (𝑏 = 𝐵 → (𝐺‘𝑏) = (𝐺‘𝐵)) |
34 | 32, 33 | breq12d 4666 |
. . . . 5
⊢ (𝑏 = 𝐵 → ((𝐹‘𝑏) ≤ (𝐺‘𝑏) ↔ (𝐹‘𝐵) ≤ (𝐺‘𝐵))) |
35 | 34 | imbi2d 330 |
. . . 4
⊢ (𝑏 = 𝐵 → ((𝐴 ∈ ℕ → (𝐹‘𝑏) ≤ (𝐺‘𝑏)) ↔ (𝐴 ∈ ℕ → (𝐹‘𝐵) ≤ (𝐺‘𝐵)))) |
36 | | nnnn0 11299 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ0) |
37 | | faccl 13070 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℕ0
→ (!‘𝐴) ∈
ℕ) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℕ →
(!‘𝐴) ∈
ℕ) |
39 | 38 | nnzd 11481 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℕ →
(!‘𝐴) ∈
ℤ) |
40 | 39 | znegcld 11484 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ →
-(!‘𝐴) ∈
ℤ) |
41 | | rpexpcl 12879 |
. . . . . . . . . 10
⊢ ((2
∈ ℝ+ ∧ -(!‘𝐴) ∈ ℤ) →
(2↑-(!‘𝐴))
∈ ℝ+) |
42 | 9, 40, 41 | sylancr 695 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ →
(2↑-(!‘𝐴))
∈ ℝ+) |
43 | 42 | rpred 11872 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ →
(2↑-(!‘𝐴))
∈ ℝ) |
44 | 43 | leidd 10594 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ →
(2↑-(!‘𝐴)) ≤
(2↑-(!‘𝐴))) |
45 | | nncn 11028 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℂ) |
46 | 45 | subidd 10380 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℕ → (𝐴 − 𝐴) = 0) |
47 | 46 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ → ((1 /
2)↑(𝐴 − 𝐴)) = ((1 /
2)↑0)) |
48 | | halfcn 11247 |
. . . . . . . . . . 11
⊢ (1 / 2)
∈ ℂ |
49 | | exp0 12864 |
. . . . . . . . . . 11
⊢ ((1 / 2)
∈ ℂ → ((1 / 2)↑0) = 1) |
50 | 48, 49 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((1 /
2)↑0) = 1 |
51 | 47, 50 | syl6eq 2672 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ → ((1 /
2)↑(𝐴 − 𝐴)) = 1) |
52 | 51 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ →
((2↑-(!‘𝐴))
· ((1 / 2)↑(𝐴
− 𝐴))) =
((2↑-(!‘𝐴))
· 1)) |
53 | 42 | rpcnd 11874 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ →
(2↑-(!‘𝐴))
∈ ℂ) |
54 | 53 | mulid1d 10057 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ →
((2↑-(!‘𝐴))
· 1) = (2↑-(!‘𝐴))) |
55 | 52, 54 | eqtrd 2656 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ →
((2↑-(!‘𝐴))
· ((1 / 2)↑(𝐴
− 𝐴))) =
(2↑-(!‘𝐴))) |
56 | 44, 55 | breqtrrd 4681 |
. . . . . 6
⊢ (𝐴 ∈ ℕ →
(2↑-(!‘𝐴)) ≤
((2↑-(!‘𝐴))
· ((1 / 2)↑(𝐴
− 𝐴)))) |
57 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (!‘𝑎) = (!‘𝐴)) |
58 | 57 | negeqd 10275 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → -(!‘𝑎) = -(!‘𝐴)) |
59 | 58 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (2↑-(!‘𝑎)) = (2↑-(!‘𝐴))) |
60 | | ovex 6678 |
. . . . . . 7
⊢
(2↑-(!‘𝐴)) ∈ V |
61 | 59, 5, 60 | fvmpt 6282 |
. . . . . 6
⊢ (𝐴 ∈ ℕ → (𝐹‘𝐴) = (2↑-(!‘𝐴))) |
62 | | nnz 11399 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℤ) |
63 | | uzid 11702 |
. . . . . . 7
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
(ℤ≥‘𝐴)) |
64 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑐 = 𝐴 → (𝑐 − 𝐴) = (𝐴 − 𝐴)) |
65 | 64 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑐 = 𝐴 → ((1 / 2)↑(𝑐 − 𝐴)) = ((1 / 2)↑(𝐴 − 𝐴))) |
66 | 65 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑐 = 𝐴 → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴))) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴 − 𝐴)))) |
67 | | aaliou3lem.a |
. . . . . . . 8
⊢ 𝐺 = (𝑐 ∈ (ℤ≥‘𝐴) ↦
((2↑-(!‘𝐴))
· ((1 / 2)↑(𝑐
− 𝐴)))) |
68 | | ovex 6678 |
. . . . . . . 8
⊢
((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴 − 𝐴))) ∈ V |
69 | 66, 67, 68 | fvmpt 6282 |
. . . . . . 7
⊢ (𝐴 ∈
(ℤ≥‘𝐴) → (𝐺‘𝐴) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴 − 𝐴)))) |
70 | 62, 63, 69 | 3syl 18 |
. . . . . 6
⊢ (𝐴 ∈ ℕ → (𝐺‘𝐴) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴 − 𝐴)))) |
71 | 56, 61, 70 | 3brtr4d 4685 |
. . . . 5
⊢ (𝐴 ∈ ℕ → (𝐹‘𝐴) ≤ (𝐺‘𝐴)) |
72 | 71 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℤ → (𝐴 ∈ ℕ → (𝐹‘𝐴) ≤ (𝐺‘𝐴))) |
73 | | eluznn 11758 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → 𝑑 ∈ ℕ) |
74 | 73 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → 𝑑 ∈ ℕ0) |
75 | | faccl 13070 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 ∈ ℕ0
→ (!‘𝑑) ∈
ℕ) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (!‘𝑑) ∈ ℕ) |
77 | 76 | nnzd 11481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (!‘𝑑) ∈ ℤ) |
78 | 77 | znegcld 11484 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → -(!‘𝑑) ∈ ℤ) |
79 | | rpexpcl 12879 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℝ+ ∧ -(!‘𝑑) ∈ ℤ) →
(2↑-(!‘𝑑))
∈ ℝ+) |
80 | 9, 78, 79 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (2↑-(!‘𝑑)) ∈
ℝ+) |
81 | 80 | rpred 11872 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (2↑-(!‘𝑑)) ∈
ℝ) |
82 | 80 | rpge0d 11876 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → 0 ≤ (2↑-(!‘𝑑))) |
83 | | simpl 473 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → 𝐴 ∈ ℕ) |
84 | 83 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → 𝐴 ∈
ℕ0) |
85 | 84, 37 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (!‘𝐴) ∈ ℕ) |
86 | 85 | nnzd 11481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (!‘𝐴) ∈ ℤ) |
87 | 86 | znegcld 11484 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → -(!‘𝐴) ∈ ℤ) |
88 | 9, 87, 41 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (2↑-(!‘𝐴)) ∈
ℝ+) |
89 | | halfre 11246 |
. . . . . . . . . . . . . . . 16
⊢ (1 / 2)
∈ ℝ |
90 | | halfgt0 11248 |
. . . . . . . . . . . . . . . 16
⊢ 0 < (1
/ 2) |
91 | 89, 90 | elrpii 11835 |
. . . . . . . . . . . . . . 15
⊢ (1 / 2)
∈ ℝ+ |
92 | | eluzelz 11697 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 ∈
(ℤ≥‘𝐴) → 𝑑 ∈ ℤ) |
93 | | zsubcl 11419 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑑 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑑 − 𝐴) ∈ ℤ) |
94 | 92, 62, 93 | syl2anr 495 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (𝑑 − 𝐴) ∈ ℤ) |
95 | | rpexpcl 12879 |
. . . . . . . . . . . . . . 15
⊢ (((1 / 2)
∈ ℝ+ ∧ (𝑑 − 𝐴) ∈ ℤ) → ((1 /
2)↑(𝑑 − 𝐴)) ∈
ℝ+) |
96 | 91, 94, 95 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → ((1 / 2)↑(𝑑 − 𝐴)) ∈
ℝ+) |
97 | 88, 96 | rpmulcld 11888 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) ∈
ℝ+) |
98 | 97 | rpred 11872 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) ∈ ℝ) |
99 | 81, 82, 98 | jca31 557 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (((2↑-(!‘𝑑)) ∈ ℝ ∧ 0 ≤
(2↑-(!‘𝑑)))
∧ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) ∈ ℝ)) |
100 | 99 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) ∧ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴)))) → (((2↑-(!‘𝑑)) ∈ ℝ ∧ 0 ≤
(2↑-(!‘𝑑)))
∧ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) ∈ ℝ)) |
101 | 92 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → 𝑑 ∈ ℤ) |
102 | 78, 101 | zmulcld 11488 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (-(!‘𝑑) · 𝑑) ∈ ℤ) |
103 | | rpexpcl 12879 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℝ+ ∧ (-(!‘𝑑) · 𝑑) ∈ ℤ) →
(2↑(-(!‘𝑑)
· 𝑑)) ∈
ℝ+) |
104 | 9, 102, 103 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (2↑(-(!‘𝑑) · 𝑑)) ∈
ℝ+) |
105 | 104 | rpred 11872 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (2↑(-(!‘𝑑) · 𝑑)) ∈ ℝ) |
106 | 104 | rpge0d 11876 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → 0 ≤ (2↑(-(!‘𝑑) · 𝑑))) |
107 | 89 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (1 / 2) ∈
ℝ) |
108 | 105, 106,
107 | jca31 557 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (((2↑(-(!‘𝑑) · 𝑑)) ∈ ℝ ∧ 0 ≤
(2↑(-(!‘𝑑)
· 𝑑))) ∧ (1 / 2)
∈ ℝ)) |
109 | 108 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) ∧ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴)))) → (((2↑(-(!‘𝑑) · 𝑑)) ∈ ℝ ∧ 0 ≤
(2↑(-(!‘𝑑)
· 𝑑))) ∧ (1 / 2)
∈ ℝ)) |
110 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) ∧ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴)))) → (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴)))) |
111 | 76 | nncnd 11036 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (!‘𝑑) ∈ ℂ) |
112 | 101 | zcnd 11483 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → 𝑑 ∈ ℂ) |
113 | 111, 112 | mulneg1d 10483 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (-(!‘𝑑) · 𝑑) = -((!‘𝑑) · 𝑑)) |
114 | 76, 73 | nnmulcld 11068 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → ((!‘𝑑) · 𝑑) ∈ ℕ) |
115 | 114 | nnge1d 11063 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → 1 ≤ ((!‘𝑑) · 𝑑)) |
116 | | 1re 10039 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ |
117 | 114 | nnred 11035 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → ((!‘𝑑) · 𝑑) ∈ ℝ) |
118 | | leneg 10531 |
. . . . . . . . . . . . . . . . 17
⊢ ((1
∈ ℝ ∧ ((!‘𝑑) · 𝑑) ∈ ℝ) → (1 ≤
((!‘𝑑) · 𝑑) ↔ -((!‘𝑑) · 𝑑) ≤ -1)) |
119 | 116, 117,
118 | sylancr 695 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (1 ≤ ((!‘𝑑) · 𝑑) ↔ -((!‘𝑑) · 𝑑) ≤ -1)) |
120 | 115, 119 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → -((!‘𝑑) · 𝑑) ≤ -1) |
121 | 113, 120 | eqbrtrd 4675 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (-(!‘𝑑) · 𝑑) ≤ -1) |
122 | | neg1z 11413 |
. . . . . . . . . . . . . . 15
⊢ -1 ∈
ℤ |
123 | | eluz 11701 |
. . . . . . . . . . . . . . 15
⊢
(((-(!‘𝑑)
· 𝑑) ∈ ℤ
∧ -1 ∈ ℤ) → (-1 ∈
(ℤ≥‘(-(!‘𝑑) · 𝑑)) ↔ (-(!‘𝑑) · 𝑑) ≤ -1)) |
124 | 102, 122,
123 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (-1 ∈
(ℤ≥‘(-(!‘𝑑) · 𝑑)) ↔ (-(!‘𝑑) · 𝑑) ≤ -1)) |
125 | 121, 124 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → -1 ∈
(ℤ≥‘(-(!‘𝑑) · 𝑑))) |
126 | | 2re 11090 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ |
127 | | 1le2 11241 |
. . . . . . . . . . . . . 14
⊢ 1 ≤
2 |
128 | | leexp2a 12916 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℝ ∧ 1 ≤ 2 ∧ -1 ∈
(ℤ≥‘(-(!‘𝑑) · 𝑑))) → (2↑(-(!‘𝑑) · 𝑑)) ≤ (2↑-1)) |
129 | 126, 127,
128 | mp3an12 1414 |
. . . . . . . . . . . . 13
⊢ (-1
∈ (ℤ≥‘(-(!‘𝑑) · 𝑑)) → (2↑(-(!‘𝑑) · 𝑑)) ≤ (2↑-1)) |
130 | 125, 129 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (2↑(-(!‘𝑑) · 𝑑)) ≤ (2↑-1)) |
131 | | 2cn 11091 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℂ |
132 | | expn1 12870 |
. . . . . . . . . . . . 13
⊢ (2 ∈
ℂ → (2↑-1) = (1 / 2)) |
133 | 131, 132 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(2↑-1) = (1 / 2) |
134 | 130, 133 | syl6breq 4694 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (2↑(-(!‘𝑑) · 𝑑)) ≤ (1 / 2)) |
135 | 134 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) ∧ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴)))) → (2↑(-(!‘𝑑) · 𝑑)) ≤ (1 / 2)) |
136 | | lemul12a 10881 |
. . . . . . . . . . 11
⊢
(((((2↑-(!‘𝑑)) ∈ ℝ ∧ 0 ≤
(2↑-(!‘𝑑)))
∧ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) ∈ ℝ) ∧
(((2↑(-(!‘𝑑)
· 𝑑)) ∈ ℝ
∧ 0 ≤ (2↑(-(!‘𝑑) · 𝑑))) ∧ (1 / 2) ∈ ℝ)) →
(((2↑-(!‘𝑑))
≤ ((2↑-(!‘𝐴))
· ((1 / 2)↑(𝑑
− 𝐴))) ∧
(2↑(-(!‘𝑑)
· 𝑑)) ≤ (1 / 2))
→ ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))) ≤ (((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) · (1 / 2)))) |
137 | 136 | 3impia 1261 |
. . . . . . . . . 10
⊢
(((((2↑-(!‘𝑑)) ∈ ℝ ∧ 0 ≤
(2↑-(!‘𝑑)))
∧ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) ∈ ℝ) ∧
(((2↑(-(!‘𝑑)
· 𝑑)) ∈ ℝ
∧ 0 ≤ (2↑(-(!‘𝑑) · 𝑑))) ∧ (1 / 2) ∈ ℝ) ∧
((2↑-(!‘𝑑)) ≤
((2↑-(!‘𝐴))
· ((1 / 2)↑(𝑑
− 𝐴))) ∧
(2↑(-(!‘𝑑)
· 𝑑)) ≤ (1 / 2)))
→ ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))) ≤ (((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) · (1 / 2))) |
138 | 100, 109,
110, 135, 137 | syl112anc 1330 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) ∧ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴)))) → ((2↑-(!‘𝑑)) ·
(2↑(-(!‘𝑑)
· 𝑑))) ≤
(((2↑-(!‘𝐴))
· ((1 / 2)↑(𝑑
− 𝐴))) · (1 /
2))) |
139 | 138 | ex 450 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → ((2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) → ((2↑-(!‘𝑑)) ·
(2↑(-(!‘𝑑)
· 𝑑))) ≤
(((2↑-(!‘𝐴))
· ((1 / 2)↑(𝑑
− 𝐴))) · (1 /
2)))) |
140 | | facp1 13065 |
. . . . . . . . . . . . . 14
⊢ (𝑑 ∈ ℕ0
→ (!‘(𝑑 + 1)) =
((!‘𝑑) ·
(𝑑 + 1))) |
141 | 74, 140 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (!‘(𝑑 + 1)) = ((!‘𝑑) · (𝑑 + 1))) |
142 | 141 | negeqd 10275 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → -(!‘(𝑑 + 1)) = -((!‘𝑑) · (𝑑 + 1))) |
143 | | ax-1cn 9994 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
144 | | addcom 10222 |
. . . . . . . . . . . . . . 15
⊢ ((𝑑 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑑 + 1) =
(1 + 𝑑)) |
145 | 112, 143,
144 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (𝑑 + 1) = (1 + 𝑑)) |
146 | 145 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (-(!‘𝑑) · (𝑑 + 1)) = (-(!‘𝑑) · (1 + 𝑑))) |
147 | | peano2cn 10208 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 ∈ ℂ → (𝑑 + 1) ∈
ℂ) |
148 | 112, 147 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (𝑑 + 1) ∈ ℂ) |
149 | 111, 148 | mulneg1d 10483 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (-(!‘𝑑) · (𝑑 + 1)) = -((!‘𝑑) · (𝑑 + 1))) |
150 | 78 | zcnd 11483 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → -(!‘𝑑) ∈ ℂ) |
151 | | 1cnd 10056 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → 1 ∈ ℂ) |
152 | 150, 151,
112 | adddid 10064 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (-(!‘𝑑) · (1 + 𝑑)) = ((-(!‘𝑑) · 1) + (-(!‘𝑑) · 𝑑))) |
153 | 150 | mulid1d 10057 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (-(!‘𝑑) · 1) = -(!‘𝑑)) |
154 | 153 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → ((-(!‘𝑑) · 1) + (-(!‘𝑑) · 𝑑)) = (-(!‘𝑑) + (-(!‘𝑑) · 𝑑))) |
155 | 152, 154 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (-(!‘𝑑) · (1 + 𝑑)) = (-(!‘𝑑) + (-(!‘𝑑) · 𝑑))) |
156 | 146, 149,
155 | 3eqtr3d 2664 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → -((!‘𝑑) · (𝑑 + 1)) = (-(!‘𝑑) + (-(!‘𝑑) · 𝑑))) |
157 | 142, 156 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → -(!‘(𝑑 + 1)) = (-(!‘𝑑) + (-(!‘𝑑) · 𝑑))) |
158 | 157 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (2↑-(!‘(𝑑 + 1))) =
(2↑(-(!‘𝑑) +
(-(!‘𝑑) ·
𝑑)))) |
159 | | 2cnne0 11242 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
160 | | expaddz 12904 |
. . . . . . . . . . . 12
⊢ (((2
∈ ℂ ∧ 2 ≠ 0) ∧ (-(!‘𝑑) ∈ ℤ ∧ (-(!‘𝑑) · 𝑑) ∈ ℤ)) →
(2↑(-(!‘𝑑) +
(-(!‘𝑑) ·
𝑑))) =
((2↑-(!‘𝑑))
· (2↑(-(!‘𝑑) · 𝑑)))) |
161 | 159, 160 | mpan 706 |
. . . . . . . . . . 11
⊢
((-(!‘𝑑)
∈ ℤ ∧ (-(!‘𝑑) · 𝑑) ∈ ℤ) →
(2↑(-(!‘𝑑) +
(-(!‘𝑑) ·
𝑑))) =
((2↑-(!‘𝑑))
· (2↑(-(!‘𝑑) · 𝑑)))) |
162 | 78, 102, 161 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (2↑(-(!‘𝑑) + (-(!‘𝑑) · 𝑑))) = ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑)))) |
163 | 158, 162 | eqtrd 2656 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (2↑-(!‘(𝑑 + 1))) =
((2↑-(!‘𝑑))
· (2↑(-(!‘𝑑) · 𝑑)))) |
164 | 45 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → 𝐴 ∈ ℂ) |
165 | 112, 151,
164 | addsubd 10413 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → ((𝑑 + 1) − 𝐴) = ((𝑑 − 𝐴) + 1)) |
166 | 165 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → ((1 / 2)↑((𝑑 + 1) − 𝐴)) = ((1 / 2)↑((𝑑 − 𝐴) + 1))) |
167 | | uznn0sub 11719 |
. . . . . . . . . . . . . 14
⊢ (𝑑 ∈
(ℤ≥‘𝐴) → (𝑑 − 𝐴) ∈
ℕ0) |
168 | 167 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (𝑑 − 𝐴) ∈
ℕ0) |
169 | | expp1 12867 |
. . . . . . . . . . . . 13
⊢ (((1 / 2)
∈ ℂ ∧ (𝑑
− 𝐴) ∈
ℕ0) → ((1 / 2)↑((𝑑 − 𝐴) + 1)) = (((1 / 2)↑(𝑑 − 𝐴)) · (1 / 2))) |
170 | 48, 168, 169 | sylancr 695 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → ((1 / 2)↑((𝑑 − 𝐴) + 1)) = (((1 / 2)↑(𝑑 − 𝐴)) · (1 / 2))) |
171 | 166, 170 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → ((1 / 2)↑((𝑑 + 1) − 𝐴)) = (((1 / 2)↑(𝑑 − 𝐴)) · (1 / 2))) |
172 | 171 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → ((2↑-(!‘𝐴)) · ((1 /
2)↑((𝑑 + 1) −
𝐴))) =
((2↑-(!‘𝐴))
· (((1 / 2)↑(𝑑
− 𝐴)) · (1 /
2)))) |
173 | 88 | rpcnd 11874 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (2↑-(!‘𝐴)) ∈
ℂ) |
174 | 96 | rpcnd 11874 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → ((1 / 2)↑(𝑑 − 𝐴)) ∈ ℂ) |
175 | 48 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (1 / 2) ∈
ℂ) |
176 | 173, 174,
175 | mulassd 10063 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) · (1 / 2)) =
((2↑-(!‘𝐴))
· (((1 / 2)↑(𝑑
− 𝐴)) · (1 /
2)))) |
177 | 172, 176 | eqtr4d 2659 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → ((2↑-(!‘𝐴)) · ((1 /
2)↑((𝑑 + 1) −
𝐴))) =
(((2↑-(!‘𝐴))
· ((1 / 2)↑(𝑑
− 𝐴))) · (1 /
2))) |
178 | 163, 177 | breq12d 4666 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → ((2↑-(!‘(𝑑 + 1))) ≤
((2↑-(!‘𝐴))
· ((1 / 2)↑((𝑑
+ 1) − 𝐴))) ↔
((2↑-(!‘𝑑))
· (2↑(-(!‘𝑑) · 𝑑))) ≤ (((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) · (1 / 2)))) |
179 | 139, 178 | sylibrd 249 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → ((2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) → (2↑-(!‘(𝑑 + 1))) ≤
((2↑-(!‘𝐴))
· ((1 / 2)↑((𝑑
+ 1) − 𝐴))))) |
180 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑑 → (!‘𝑎) = (!‘𝑑)) |
181 | 180 | negeqd 10275 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑑 → -(!‘𝑎) = -(!‘𝑑)) |
182 | 181 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑑 → (2↑-(!‘𝑎)) = (2↑-(!‘𝑑))) |
183 | | ovex 6678 |
. . . . . . . . . 10
⊢
(2↑-(!‘𝑑)) ∈ V |
184 | 182, 5, 183 | fvmpt 6282 |
. . . . . . . . 9
⊢ (𝑑 ∈ ℕ → (𝐹‘𝑑) = (2↑-(!‘𝑑))) |
185 | 73, 184 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝑑) = (2↑-(!‘𝑑))) |
186 | | oveq1 6657 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑑 → (𝑐 − 𝐴) = (𝑑 − 𝐴)) |
187 | 186 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑑 → ((1 / 2)↑(𝑐 − 𝐴)) = ((1 / 2)↑(𝑑 − 𝐴))) |
188 | 187 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑑 → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴))) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴)))) |
189 | | ovex 6678 |
. . . . . . . . . 10
⊢
((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) ∈ V |
190 | 188, 67, 189 | fvmpt 6282 |
. . . . . . . . 9
⊢ (𝑑 ∈
(ℤ≥‘𝐴) → (𝐺‘𝑑) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴)))) |
191 | 190 | adantl 482 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (𝐺‘𝑑) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴)))) |
192 | 185, 191 | breq12d 4666 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → ((𝐹‘𝑑) ≤ (𝐺‘𝑑) ↔ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))))) |
193 | 73 | peano2nnd 11037 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (𝑑 + 1) ∈ ℕ) |
194 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑑 + 1) → (!‘𝑎) = (!‘(𝑑 + 1))) |
195 | 194 | negeqd 10275 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑑 + 1) → -(!‘𝑎) = -(!‘(𝑑 + 1))) |
196 | 195 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑑 + 1) → (2↑-(!‘𝑎)) = (2↑-(!‘(𝑑 + 1)))) |
197 | | ovex 6678 |
. . . . . . . . . 10
⊢
(2↑-(!‘(𝑑
+ 1))) ∈ V |
198 | 196, 5, 197 | fvmpt 6282 |
. . . . . . . . 9
⊢ ((𝑑 + 1) ∈ ℕ →
(𝐹‘(𝑑 + 1)) =
(2↑-(!‘(𝑑 +
1)))) |
199 | 193, 198 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (𝐹‘(𝑑 + 1)) = (2↑-(!‘(𝑑 + 1)))) |
200 | | peano2uz 11741 |
. . . . . . . . . 10
⊢ (𝑑 ∈
(ℤ≥‘𝐴) → (𝑑 + 1) ∈
(ℤ≥‘𝐴)) |
201 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑐 = (𝑑 + 1) → (𝑐 − 𝐴) = ((𝑑 + 1) − 𝐴)) |
202 | 201 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑐 = (𝑑 + 1) → ((1 / 2)↑(𝑐 − 𝐴)) = ((1 / 2)↑((𝑑 + 1) − 𝐴))) |
203 | 202 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑐 = (𝑑 + 1) → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴))) = ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴)))) |
204 | | ovex 6678 |
. . . . . . . . . . 11
⊢
((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))) ∈ V |
205 | 203, 67, 204 | fvmpt 6282 |
. . . . . . . . . 10
⊢ ((𝑑 + 1) ∈
(ℤ≥‘𝐴) → (𝐺‘(𝑑 + 1)) = ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴)))) |
206 | 200, 205 | syl 17 |
. . . . . . . . 9
⊢ (𝑑 ∈
(ℤ≥‘𝐴) → (𝐺‘(𝑑 + 1)) = ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴)))) |
207 | 206 | adantl 482 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → (𝐺‘(𝑑 + 1)) = ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴)))) |
208 | 199, 207 | breq12d 4666 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → ((𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1)) ↔ (2↑-(!‘(𝑑 + 1))) ≤
((2↑-(!‘𝐴))
· ((1 / 2)↑((𝑑
+ 1) − 𝐴))))) |
209 | 179, 192,
208 | 3imtr4d 283 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈
(ℤ≥‘𝐴)) → ((𝐹‘𝑑) ≤ (𝐺‘𝑑) → (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1)))) |
210 | 209 | expcom 451 |
. . . . 5
⊢ (𝑑 ∈
(ℤ≥‘𝐴) → (𝐴 ∈ ℕ → ((𝐹‘𝑑) ≤ (𝐺‘𝑑) → (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1))))) |
211 | 210 | a2d 29 |
. . . 4
⊢ (𝑑 ∈
(ℤ≥‘𝐴) → ((𝐴 ∈ ℕ → (𝐹‘𝑑) ≤ (𝐺‘𝑑)) → (𝐴 ∈ ℕ → (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1))))) |
212 | 23, 27, 31, 35, 72, 211 | uzind4 11746 |
. . 3
⊢ (𝐵 ∈
(ℤ≥‘𝐴) → (𝐴 ∈ ℕ → (𝐹‘𝐵) ≤ (𝐺‘𝐵))) |
213 | 212 | impcom 446 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝐵) ≤ (𝐺‘𝐵)) |
214 | | 0xr 10086 |
. . 3
⊢ 0 ∈
ℝ* |
215 | 67 | aaliou3lem1 24097 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈
(ℤ≥‘𝐴)) → (𝐺‘𝐵) ∈ ℝ) |
216 | | elioc2 12236 |
. . 3
⊢ ((0
∈ ℝ* ∧ (𝐺‘𝐵) ∈ ℝ) → ((𝐹‘𝐵) ∈ (0(,](𝐺‘𝐵)) ↔ ((𝐹‘𝐵) ∈ ℝ ∧ 0 < (𝐹‘𝐵) ∧ (𝐹‘𝐵) ≤ (𝐺‘𝐵)))) |
217 | 214, 215,
216 | sylancr 695 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈
(ℤ≥‘𝐴)) → ((𝐹‘𝐵) ∈ (0(,](𝐺‘𝐵)) ↔ ((𝐹‘𝐵) ∈ ℝ ∧ 0 < (𝐹‘𝐵) ∧ (𝐹‘𝐵) ≤ (𝐺‘𝐵)))) |
218 | 18, 19, 213, 217 | mpbir3and 1245 |
1
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝐵) ∈ (0(,](𝐺‘𝐵))) |