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

Theorem aaliou3lem2 25825
Description: Lemma for aaliou3 25833. (Contributed by Stefan O'Rear, 16-Nov-2014.)
Hypotheses
Ref Expression
aaliou3lem.a 𝐺 = (𝑐 ∈ (ℤ𝐴) ↦ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐𝐴))))
aaliou3lem.b 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))
Assertion
Ref Expression
aaliou3lem2 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → (𝐹𝐵) ∈ (0(,](𝐺𝐵)))
Distinct variable groups:   𝐹,𝑐   𝐴,𝑎,𝑐   𝐵,𝑎,𝑐   𝐺,𝑎
Allowed substitution hints:   𝐹(𝑎)   𝐺(𝑐)

Proof of Theorem aaliou3lem2
Dummy variables 𝑏 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eluznn 12889 . . . . 5 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → 𝐵 ∈ ℕ)
2 fveq2 6881 . . . . . . . 8 (𝑎 = 𝐵 → (!‘𝑎) = (!‘𝐵))
32negeqd 11441 . . . . . . 7 (𝑎 = 𝐵 → -(!‘𝑎) = -(!‘𝐵))
43oveq2d 7412 . . . . . 6 (𝑎 = 𝐵 → (2↑-(!‘𝑎)) = (2↑-(!‘𝐵)))
5 aaliou3lem.b . . . . . 6 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))
6 ovex 7429 . . . . . 6 (2↑-(!‘𝐵)) ∈ V
74, 5, 6fvmpt 6987 . . . . 5 (𝐵 ∈ ℕ → (𝐹𝐵) = (2↑-(!‘𝐵)))
81, 7syl 17 . . . 4 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → (𝐹𝐵) = (2↑-(!‘𝐵)))
9 2rp 12966 . . . . 5 2 ∈ ℝ+
101nnnn0d 12519 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → 𝐵 ∈ ℕ0)
1110faccld 14231 . . . . . . 7 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → (!‘𝐵) ∈ ℕ)
1211nnzd 12572 . . . . . 6 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → (!‘𝐵) ∈ ℤ)
1312znegcld 12655 . . . . 5 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → -(!‘𝐵) ∈ ℤ)
14 rpexpcl 14033 . . . . 5 ((2 ∈ ℝ+ ∧ -(!‘𝐵) ∈ ℤ) → (2↑-(!‘𝐵)) ∈ ℝ+)
159, 13, 14sylancr 588 . . . 4 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → (2↑-(!‘𝐵)) ∈ ℝ+)
168, 15eqeltrd 2834 . . 3 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → (𝐹𝐵) ∈ ℝ+)
1716rpred 13003 . 2 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → (𝐹𝐵) ∈ ℝ)
1816rpgt0d 13006 . 2 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → 0 < (𝐹𝐵))
19 fveq2 6881 . . . . . 6 (𝑏 = 𝐴 → (𝐹𝑏) = (𝐹𝐴))
20 fveq2 6881 . . . . . 6 (𝑏 = 𝐴 → (𝐺𝑏) = (𝐺𝐴))
2119, 20breq12d 5157 . . . . 5 (𝑏 = 𝐴 → ((𝐹𝑏) ≤ (𝐺𝑏) ↔ (𝐹𝐴) ≤ (𝐺𝐴)))
2221imbi2d 341 . . . 4 (𝑏 = 𝐴 → ((𝐴 ∈ ℕ → (𝐹𝑏) ≤ (𝐺𝑏)) ↔ (𝐴 ∈ ℕ → (𝐹𝐴) ≤ (𝐺𝐴))))
23 fveq2 6881 . . . . . 6 (𝑏 = 𝑑 → (𝐹𝑏) = (𝐹𝑑))
24 fveq2 6881 . . . . . 6 (𝑏 = 𝑑 → (𝐺𝑏) = (𝐺𝑑))
2523, 24breq12d 5157 . . . . 5 (𝑏 = 𝑑 → ((𝐹𝑏) ≤ (𝐺𝑏) ↔ (𝐹𝑑) ≤ (𝐺𝑑)))
2625imbi2d 341 . . . 4 (𝑏 = 𝑑 → ((𝐴 ∈ ℕ → (𝐹𝑏) ≤ (𝐺𝑏)) ↔ (𝐴 ∈ ℕ → (𝐹𝑑) ≤ (𝐺𝑑))))
27 fveq2 6881 . . . . . 6 (𝑏 = (𝑑 + 1) → (𝐹𝑏) = (𝐹‘(𝑑 + 1)))
28 fveq2 6881 . . . . . 6 (𝑏 = (𝑑 + 1) → (𝐺𝑏) = (𝐺‘(𝑑 + 1)))
2927, 28breq12d 5157 . . . . 5 (𝑏 = (𝑑 + 1) → ((𝐹𝑏) ≤ (𝐺𝑏) ↔ (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1))))
3029imbi2d 341 . . . 4 (𝑏 = (𝑑 + 1) → ((𝐴 ∈ ℕ → (𝐹𝑏) ≤ (𝐺𝑏)) ↔ (𝐴 ∈ ℕ → (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1)))))
31 fveq2 6881 . . . . . 6 (𝑏 = 𝐵 → (𝐹𝑏) = (𝐹𝐵))
32 fveq2 6881 . . . . . 6 (𝑏 = 𝐵 → (𝐺𝑏) = (𝐺𝐵))
3331, 32breq12d 5157 . . . . 5 (𝑏 = 𝐵 → ((𝐹𝑏) ≤ (𝐺𝑏) ↔ (𝐹𝐵) ≤ (𝐺𝐵)))
3433imbi2d 341 . . . 4 (𝑏 = 𝐵 → ((𝐴 ∈ ℕ → (𝐹𝑏) ≤ (𝐺𝑏)) ↔ (𝐴 ∈ ℕ → (𝐹𝐵) ≤ (𝐺𝐵))))
35 nnnn0 12466 . . . . . . . . . . . 12 (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)
3635faccld 14231 . . . . . . . . . . 11 (𝐴 ∈ ℕ → (!‘𝐴) ∈ ℕ)
3736nnzd 12572 . . . . . . . . . 10 (𝐴 ∈ ℕ → (!‘𝐴) ∈ ℤ)
3837znegcld 12655 . . . . . . . . 9 (𝐴 ∈ ℕ → -(!‘𝐴) ∈ ℤ)
39 rpexpcl 14033 . . . . . . . . 9 ((2 ∈ ℝ+ ∧ -(!‘𝐴) ∈ ℤ) → (2↑-(!‘𝐴)) ∈ ℝ+)
409, 38, 39sylancr 588 . . . . . . . 8 (𝐴 ∈ ℕ → (2↑-(!‘𝐴)) ∈ ℝ+)
4140rpred 13003 . . . . . . 7 (𝐴 ∈ ℕ → (2↑-(!‘𝐴)) ∈ ℝ)
4241leidd 11767 . . . . . 6 (𝐴 ∈ ℕ → (2↑-(!‘𝐴)) ≤ (2↑-(!‘𝐴)))
43 nncn 12207 . . . . . . . . . . 11 (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
4443subidd 11546 . . . . . . . . . 10 (𝐴 ∈ ℕ → (𝐴𝐴) = 0)
4544oveq2d 7412 . . . . . . . . 9 (𝐴 ∈ ℕ → ((1 / 2)↑(𝐴𝐴)) = ((1 / 2)↑0))
46 halfcn 12414 . . . . . . . . . 10 (1 / 2) ∈ ℂ
47 exp0 14018 . . . . . . . . . 10 ((1 / 2) ∈ ℂ → ((1 / 2)↑0) = 1)
4846, 47ax-mp 5 . . . . . . . . 9 ((1 / 2)↑0) = 1
4945, 48eqtrdi 2789 . . . . . . . 8 (𝐴 ∈ ℕ → ((1 / 2)↑(𝐴𝐴)) = 1)
5049oveq2d 7412 . . . . . . 7 (𝐴 ∈ ℕ → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴𝐴))) = ((2↑-(!‘𝐴)) · 1))
5140rpcnd 13005 . . . . . . . 8 (𝐴 ∈ ℕ → (2↑-(!‘𝐴)) ∈ ℂ)
5251mulridd 11218 . . . . . . 7 (𝐴 ∈ ℕ → ((2↑-(!‘𝐴)) · 1) = (2↑-(!‘𝐴)))
5350, 52eqtrd 2773 . . . . . 6 (𝐴 ∈ ℕ → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴𝐴))) = (2↑-(!‘𝐴)))
5442, 53breqtrrd 5172 . . . . 5 (𝐴 ∈ ℕ → (2↑-(!‘𝐴)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴𝐴))))
55 fveq2 6881 . . . . . . . 8 (𝑎 = 𝐴 → (!‘𝑎) = (!‘𝐴))
5655negeqd 11441 . . . . . . 7 (𝑎 = 𝐴 → -(!‘𝑎) = -(!‘𝐴))
5756oveq2d 7412 . . . . . 6 (𝑎 = 𝐴 → (2↑-(!‘𝑎)) = (2↑-(!‘𝐴)))
58 ovex 7429 . . . . . 6 (2↑-(!‘𝐴)) ∈ V
5957, 5, 58fvmpt 6987 . . . . 5 (𝐴 ∈ ℕ → (𝐹𝐴) = (2↑-(!‘𝐴)))
60 nnz 12566 . . . . . 6 (𝐴 ∈ ℕ → 𝐴 ∈ ℤ)
61 uzid 12824 . . . . . 6 (𝐴 ∈ ℤ → 𝐴 ∈ (ℤ𝐴))
62 oveq1 7403 . . . . . . . . 9 (𝑐 = 𝐴 → (𝑐𝐴) = (𝐴𝐴))
6362oveq2d 7412 . . . . . . . 8 (𝑐 = 𝐴 → ((1 / 2)↑(𝑐𝐴)) = ((1 / 2)↑(𝐴𝐴)))
6463oveq2d 7412 . . . . . . 7 (𝑐 = 𝐴 → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐𝐴))) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴𝐴))))
65 aaliou3lem.a . . . . . . 7 𝐺 = (𝑐 ∈ (ℤ𝐴) ↦ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐𝐴))))
66 ovex 7429 . . . . . . 7 ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴𝐴))) ∈ V
6764, 65, 66fvmpt 6987 . . . . . 6 (𝐴 ∈ (ℤ𝐴) → (𝐺𝐴) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴𝐴))))
6860, 61, 673syl 18 . . . . 5 (𝐴 ∈ ℕ → (𝐺𝐴) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴𝐴))))
6954, 59, 683brtr4d 5176 . . . 4 (𝐴 ∈ ℕ → (𝐹𝐴) ≤ (𝐺𝐴))
70 eluznn 12889 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 𝑑 ∈ ℕ)
7170nnnn0d 12519 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 𝑑 ∈ ℕ0)
7271faccld 14231 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (!‘𝑑) ∈ ℕ)
7372nnzd 12572 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (!‘𝑑) ∈ ℤ)
7473znegcld 12655 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → -(!‘𝑑) ∈ ℤ)
75 rpexpcl 14033 . . . . . . . . . . . . . 14 ((2 ∈ ℝ+ ∧ -(!‘𝑑) ∈ ℤ) → (2↑-(!‘𝑑)) ∈ ℝ+)
769, 74, 75sylancr 588 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑-(!‘𝑑)) ∈ ℝ+)
7776rpred 13003 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑-(!‘𝑑)) ∈ ℝ)
7876rpge0d 13007 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 0 ≤ (2↑-(!‘𝑑)))
79 simpl 484 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 𝐴 ∈ ℕ)
8079nnnn0d 12519 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 𝐴 ∈ ℕ0)
8180faccld 14231 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (!‘𝐴) ∈ ℕ)
8281nnzd 12572 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (!‘𝐴) ∈ ℤ)
8382znegcld 12655 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → -(!‘𝐴) ∈ ℤ)
849, 83, 39sylancr 588 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑-(!‘𝐴)) ∈ ℝ+)
85 halfre 12413 . . . . . . . . . . . . . . . 16 (1 / 2) ∈ ℝ
86 halfgt0 12415 . . . . . . . . . . . . . . . 16 0 < (1 / 2)
8785, 86elrpii 12964 . . . . . . . . . . . . . . 15 (1 / 2) ∈ ℝ+
88 eluzelz 12819 . . . . . . . . . . . . . . . 16 (𝑑 ∈ (ℤ𝐴) → 𝑑 ∈ ℤ)
89 zsubcl 12591 . . . . . . . . . . . . . . . 16 ((𝑑 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑑𝐴) ∈ ℤ)
9088, 60, 89syl2anr 598 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (𝑑𝐴) ∈ ℤ)
91 rpexpcl 14033 . . . . . . . . . . . . . . 15 (((1 / 2) ∈ ℝ+ ∧ (𝑑𝐴) ∈ ℤ) → ((1 / 2)↑(𝑑𝐴)) ∈ ℝ+)
9287, 90, 91sylancr 588 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((1 / 2)↑(𝑑𝐴)) ∈ ℝ+)
9384, 92rpmulcld 13019 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) ∈ ℝ+)
9493rpred 13003 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) ∈ ℝ)
9577, 78, 94jca31 516 . . . . . . . . . . 11 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (((2↑-(!‘𝑑)) ∈ ℝ ∧ 0 ≤ (2↑-(!‘𝑑))) ∧ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) ∈ ℝ))
9695adantr 482 . . . . . . . . . 10 (((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) ∧ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴)))) → (((2↑-(!‘𝑑)) ∈ ℝ ∧ 0 ≤ (2↑-(!‘𝑑))) ∧ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) ∈ ℝ))
9788adantl 483 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 𝑑 ∈ ℤ)
9874, 97zmulcld 12659 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (-(!‘𝑑) · 𝑑) ∈ ℤ)
99 rpexpcl 14033 . . . . . . . . . . . . . 14 ((2 ∈ ℝ+ ∧ (-(!‘𝑑) · 𝑑) ∈ ℤ) → (2↑(-(!‘𝑑) · 𝑑)) ∈ ℝ+)
1009, 98, 99sylancr 588 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑(-(!‘𝑑) · 𝑑)) ∈ ℝ+)
101100rpred 13003 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑(-(!‘𝑑) · 𝑑)) ∈ ℝ)
102100rpge0d 13007 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 0 ≤ (2↑(-(!‘𝑑) · 𝑑)))
10385a1i 11 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (1 / 2) ∈ ℝ)
104101, 102, 103jca31 516 . . . . . . . . . . 11 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (((2↑(-(!‘𝑑) · 𝑑)) ∈ ℝ ∧ 0 ≤ (2↑(-(!‘𝑑) · 𝑑))) ∧ (1 / 2) ∈ ℝ))
105104adantr 482 . . . . . . . . . 10 (((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) ∧ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴)))) → (((2↑(-(!‘𝑑) · 𝑑)) ∈ ℝ ∧ 0 ≤ (2↑(-(!‘𝑑) · 𝑑))) ∧ (1 / 2) ∈ ℝ))
106 simpr 486 . . . . . . . . . 10 (((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) ∧ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴)))) → (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))))
107 2re 12273 . . . . . . . . . . . . 13 2 ∈ ℝ
108 1le2 12408 . . . . . . . . . . . . 13 1 ≤ 2
10972nncnd 12215 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (!‘𝑑) ∈ ℂ)
11097zcnd 12654 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 𝑑 ∈ ℂ)
111109, 110mulneg1d 11654 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (-(!‘𝑑) · 𝑑) = -((!‘𝑑) · 𝑑))
11272, 70nnmulcld 12252 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((!‘𝑑) · 𝑑) ∈ ℕ)
113112nnge1d 12247 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 1 ≤ ((!‘𝑑) · 𝑑))
114 1re 11201 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
115112nnred 12214 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((!‘𝑑) · 𝑑) ∈ ℝ)
116 leneg 11704 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ ((!‘𝑑) · 𝑑) ∈ ℝ) → (1 ≤ ((!‘𝑑) · 𝑑) ↔ -((!‘𝑑) · 𝑑) ≤ -1))
117114, 115, 116sylancr 588 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (1 ≤ ((!‘𝑑) · 𝑑) ↔ -((!‘𝑑) · 𝑑) ≤ -1))
118113, 117mpbid 231 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → -((!‘𝑑) · 𝑑) ≤ -1)
119111, 118eqbrtrd 5166 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (-(!‘𝑑) · 𝑑) ≤ -1)
120 neg1z 12585 . . . . . . . . . . . . . . 15 -1 ∈ ℤ
121 eluz 12823 . . . . . . . . . . . . . . 15 (((-(!‘𝑑) · 𝑑) ∈ ℤ ∧ -1 ∈ ℤ) → (-1 ∈ (ℤ‘(-(!‘𝑑) · 𝑑)) ↔ (-(!‘𝑑) · 𝑑) ≤ -1))
12298, 120, 121sylancl 587 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (-1 ∈ (ℤ‘(-(!‘𝑑) · 𝑑)) ↔ (-(!‘𝑑) · 𝑑) ≤ -1))
123119, 122mpbird 257 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → -1 ∈ (ℤ‘(-(!‘𝑑) · 𝑑)))
124 leexp2a 14124 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ 1 ≤ 2 ∧ -1 ∈ (ℤ‘(-(!‘𝑑) · 𝑑))) → (2↑(-(!‘𝑑) · 𝑑)) ≤ (2↑-1))
125107, 108, 123, 124mp3an12i 1466 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑(-(!‘𝑑) · 𝑑)) ≤ (2↑-1))
126 2cn 12274 . . . . . . . . . . . . 13 2 ∈ ℂ
127 expn1 14024 . . . . . . . . . . . . 13 (2 ∈ ℂ → (2↑-1) = (1 / 2))
128126, 127ax-mp 5 . . . . . . . . . . . 12 (2↑-1) = (1 / 2)
129125, 128breqtrdi 5185 . . . . . . . . . . 11 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑(-(!‘𝑑) · 𝑑)) ≤ (1 / 2))
130129adantr 482 . . . . . . . . . 10 (((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) ∧ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴)))) → (2↑(-(!‘𝑑) · 𝑑)) ≤ (1 / 2))
131 lemul12a 12059 . . . . . . . . . . 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))))
1321313impia 1118 . . . . . . . . . 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)))
13396, 105, 106, 130, 132syl112anc 1375 . . . . . . . . 9 (((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) ∧ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴)))) → ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))) ≤ (((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) · (1 / 2)))
134133ex 414 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) → ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))) ≤ (((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) · (1 / 2))))
135 facp1 14225 . . . . . . . . . . . . . 14 (𝑑 ∈ ℕ0 → (!‘(𝑑 + 1)) = ((!‘𝑑) · (𝑑 + 1)))
13671, 135syl 17 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (!‘(𝑑 + 1)) = ((!‘𝑑) · (𝑑 + 1)))
137136negeqd 11441 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → -(!‘(𝑑 + 1)) = -((!‘𝑑) · (𝑑 + 1)))
138 ax-1cn 11155 . . . . . . . . . . . . . . 15 1 ∈ ℂ
139 addcom 11387 . . . . . . . . . . . . . . 15 ((𝑑 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑑 + 1) = (1 + 𝑑))
140110, 138, 139sylancl 587 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (𝑑 + 1) = (1 + 𝑑))
141140oveq2d 7412 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (-(!‘𝑑) · (𝑑 + 1)) = (-(!‘𝑑) · (1 + 𝑑)))
142 peano2cn 11373 . . . . . . . . . . . . . . 15 (𝑑 ∈ ℂ → (𝑑 + 1) ∈ ℂ)
143110, 142syl 17 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (𝑑 + 1) ∈ ℂ)
144109, 143mulneg1d 11654 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (-(!‘𝑑) · (𝑑 + 1)) = -((!‘𝑑) · (𝑑 + 1)))
14574zcnd 12654 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → -(!‘𝑑) ∈ ℂ)
146 1cnd 11196 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 1 ∈ ℂ)
147145, 146, 110adddid 11225 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (-(!‘𝑑) · (1 + 𝑑)) = ((-(!‘𝑑) · 1) + (-(!‘𝑑) · 𝑑)))
148145mulridd 11218 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (-(!‘𝑑) · 1) = -(!‘𝑑))
149148oveq1d 7411 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((-(!‘𝑑) · 1) + (-(!‘𝑑) · 𝑑)) = (-(!‘𝑑) + (-(!‘𝑑) · 𝑑)))
150147, 149eqtrd 2773 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (-(!‘𝑑) · (1 + 𝑑)) = (-(!‘𝑑) + (-(!‘𝑑) · 𝑑)))
151141, 144, 1503eqtr3d 2781 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → -((!‘𝑑) · (𝑑 + 1)) = (-(!‘𝑑) + (-(!‘𝑑) · 𝑑)))
152137, 151eqtrd 2773 . . . . . . . . . . 11 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → -(!‘(𝑑 + 1)) = (-(!‘𝑑) + (-(!‘𝑑) · 𝑑)))
153152oveq2d 7412 . . . . . . . . . 10 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑-(!‘(𝑑 + 1))) = (2↑(-(!‘𝑑) + (-(!‘𝑑) · 𝑑))))
154 2cnne0 12409 . . . . . . . . . . . 12 (2 ∈ ℂ ∧ 2 ≠ 0)
155 expaddz 14059 . . . . . . . . . . . 12 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (-(!‘𝑑) ∈ ℤ ∧ (-(!‘𝑑) · 𝑑) ∈ ℤ)) → (2↑(-(!‘𝑑) + (-(!‘𝑑) · 𝑑))) = ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))))
156154, 155mpan 689 . . . . . . . . . . 11 ((-(!‘𝑑) ∈ ℤ ∧ (-(!‘𝑑) · 𝑑) ∈ ℤ) → (2↑(-(!‘𝑑) + (-(!‘𝑑) · 𝑑))) = ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))))
15774, 98, 156syl2anc 585 . . . . . . . . . 10 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑(-(!‘𝑑) + (-(!‘𝑑) · 𝑑))) = ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))))
158153, 157eqtrd 2773 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑-(!‘(𝑑 + 1))) = ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))))
15943adantr 482 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 𝐴 ∈ ℂ)
160110, 146, 159addsubd 11579 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((𝑑 + 1) − 𝐴) = ((𝑑𝐴) + 1))
161160oveq2d 7412 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((1 / 2)↑((𝑑 + 1) − 𝐴)) = ((1 / 2)↑((𝑑𝐴) + 1)))
162 uznn0sub 12848 . . . . . . . . . . . . . 14 (𝑑 ∈ (ℤ𝐴) → (𝑑𝐴) ∈ ℕ0)
163162adantl 483 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (𝑑𝐴) ∈ ℕ0)
164 expp1 14021 . . . . . . . . . . . . 13 (((1 / 2) ∈ ℂ ∧ (𝑑𝐴) ∈ ℕ0) → ((1 / 2)↑((𝑑𝐴) + 1)) = (((1 / 2)↑(𝑑𝐴)) · (1 / 2)))
16546, 163, 164sylancr 588 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((1 / 2)↑((𝑑𝐴) + 1)) = (((1 / 2)↑(𝑑𝐴)) · (1 / 2)))
166161, 165eqtrd 2773 . . . . . . . . . . 11 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((1 / 2)↑((𝑑 + 1) − 𝐴)) = (((1 / 2)↑(𝑑𝐴)) · (1 / 2)))
167166oveq2d 7412 . . . . . . . . . 10 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))) = ((2↑-(!‘𝐴)) · (((1 / 2)↑(𝑑𝐴)) · (1 / 2))))
16884rpcnd 13005 . . . . . . . . . . 11 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑-(!‘𝐴)) ∈ ℂ)
16992rpcnd 13005 . . . . . . . . . . 11 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((1 / 2)↑(𝑑𝐴)) ∈ ℂ)
17046a1i 11 . . . . . . . . . . 11 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (1 / 2) ∈ ℂ)
171168, 169, 170mulassd 11224 . . . . . . . . . 10 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) · (1 / 2)) = ((2↑-(!‘𝐴)) · (((1 / 2)↑(𝑑𝐴)) · (1 / 2))))
172167, 171eqtr4d 2776 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))) = (((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) · (1 / 2)))
173158, 172breq12d 5157 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((2↑-(!‘(𝑑 + 1))) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))) ↔ ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))) ≤ (((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) · (1 / 2))))
174134, 173sylibrd 259 . . . . . . 7 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) → (2↑-(!‘(𝑑 + 1))) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴)))))
175 fveq2 6881 . . . . . . . . . . . 12 (𝑎 = 𝑑 → (!‘𝑎) = (!‘𝑑))
176175negeqd 11441 . . . . . . . . . . 11 (𝑎 = 𝑑 → -(!‘𝑎) = -(!‘𝑑))
177176oveq2d 7412 . . . . . . . . . 10 (𝑎 = 𝑑 → (2↑-(!‘𝑎)) = (2↑-(!‘𝑑)))
178 ovex 7429 . . . . . . . . . 10 (2↑-(!‘𝑑)) ∈ V
179177, 5, 178fvmpt 6987 . . . . . . . . 9 (𝑑 ∈ ℕ → (𝐹𝑑) = (2↑-(!‘𝑑)))
18070, 179syl 17 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (𝐹𝑑) = (2↑-(!‘𝑑)))
181 oveq1 7403 . . . . . . . . . . . 12 (𝑐 = 𝑑 → (𝑐𝐴) = (𝑑𝐴))
182181oveq2d 7412 . . . . . . . . . . 11 (𝑐 = 𝑑 → ((1 / 2)↑(𝑐𝐴)) = ((1 / 2)↑(𝑑𝐴)))
183182oveq2d 7412 . . . . . . . . . 10 (𝑐 = 𝑑 → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐𝐴))) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))))
184 ovex 7429 . . . . . . . . . 10 ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) ∈ V
185183, 65, 184fvmpt 6987 . . . . . . . . 9 (𝑑 ∈ (ℤ𝐴) → (𝐺𝑑) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))))
186185adantl 483 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (𝐺𝑑) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))))
187180, 186breq12d 5157 . . . . . . 7 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((𝐹𝑑) ≤ (𝐺𝑑) ↔ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴)))))
18870peano2nnd 12216 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (𝑑 + 1) ∈ ℕ)
189 fveq2 6881 . . . . . . . . . . . 12 (𝑎 = (𝑑 + 1) → (!‘𝑎) = (!‘(𝑑 + 1)))
190189negeqd 11441 . . . . . . . . . . 11 (𝑎 = (𝑑 + 1) → -(!‘𝑎) = -(!‘(𝑑 + 1)))
191190oveq2d 7412 . . . . . . . . . 10 (𝑎 = (𝑑 + 1) → (2↑-(!‘𝑎)) = (2↑-(!‘(𝑑 + 1))))
192 ovex 7429 . . . . . . . . . 10 (2↑-(!‘(𝑑 + 1))) ∈ V
193191, 5, 192fvmpt 6987 . . . . . . . . 9 ((𝑑 + 1) ∈ ℕ → (𝐹‘(𝑑 + 1)) = (2↑-(!‘(𝑑 + 1))))
194188, 193syl 17 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (𝐹‘(𝑑 + 1)) = (2↑-(!‘(𝑑 + 1))))
195 peano2uz 12872 . . . . . . . . . 10 (𝑑 ∈ (ℤ𝐴) → (𝑑 + 1) ∈ (ℤ𝐴))
196 oveq1 7403 . . . . . . . . . . . . 13 (𝑐 = (𝑑 + 1) → (𝑐𝐴) = ((𝑑 + 1) − 𝐴))
197196oveq2d 7412 . . . . . . . . . . . 12 (𝑐 = (𝑑 + 1) → ((1 / 2)↑(𝑐𝐴)) = ((1 / 2)↑((𝑑 + 1) − 𝐴)))
198197oveq2d 7412 . . . . . . . . . . 11 (𝑐 = (𝑑 + 1) → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐𝐴))) = ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))))
199 ovex 7429 . . . . . . . . . . 11 ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))) ∈ V
200198, 65, 199fvmpt 6987 . . . . . . . . . 10 ((𝑑 + 1) ∈ (ℤ𝐴) → (𝐺‘(𝑑 + 1)) = ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))))
201195, 200syl 17 . . . . . . . . 9 (𝑑 ∈ (ℤ𝐴) → (𝐺‘(𝑑 + 1)) = ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))))
202201adantl 483 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (𝐺‘(𝑑 + 1)) = ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))))
203194, 202breq12d 5157 . . . . . . 7 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1)) ↔ (2↑-(!‘(𝑑 + 1))) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴)))))
204174, 187, 2033imtr4d 294 . . . . . 6 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((𝐹𝑑) ≤ (𝐺𝑑) → (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1))))
205204expcom 415 . . . . 5 (𝑑 ∈ (ℤ𝐴) → (𝐴 ∈ ℕ → ((𝐹𝑑) ≤ (𝐺𝑑) → (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1)))))
206205a2d 29 . . . 4 (𝑑 ∈ (ℤ𝐴) → ((𝐴 ∈ ℕ → (𝐹𝑑) ≤ (𝐺𝑑)) → (𝐴 ∈ ℕ → (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1)))))
20722, 26, 30, 34, 69, 206uzind4i 12881 . . 3 (𝐵 ∈ (ℤ𝐴) → (𝐴 ∈ ℕ → (𝐹𝐵) ≤ (𝐺𝐵)))
208207impcom 409 . 2 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → (𝐹𝐵) ≤ (𝐺𝐵))
209 0xr 11248 . . 3 0 ∈ ℝ*
21065aaliou3lem1 25824 . . 3 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → (𝐺𝐵) ∈ ℝ)
211 elioc2 13374 . . 3 ((0 ∈ ℝ* ∧ (𝐺𝐵) ∈ ℝ) → ((𝐹𝐵) ∈ (0(,](𝐺𝐵)) ↔ ((𝐹𝐵) ∈ ℝ ∧ 0 < (𝐹𝐵) ∧ (𝐹𝐵) ≤ (𝐺𝐵))))
212209, 210, 211sylancr 588 . 2 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → ((𝐹𝐵) ∈ (0(,](𝐺𝐵)) ↔ ((𝐹𝐵) ∈ ℝ ∧ 0 < (𝐹𝐵) ∧ (𝐹𝐵) ≤ (𝐺𝐵))))
21317, 18, 208, 212mpbir3and 1343 1 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → (𝐹𝐵) ∈ (0(,](𝐺𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wcel 2107  wne 2941   class class class wbr 5144  cmpt 5227  cfv 6535  (class class class)co 7396  cc 11095  cr 11096  0cc0 11097  1c1 11098   + caddc 11100   · cmul 11102  *cxr 11234   < clt 11235  cle 11236  cmin 11431  -cneg 11432   / cdiv 11858  cn 12199  2c2 12254  0cn0 12459  cz 12545  cuz 12809  +crp 12961  (,]cioc 13312  cexp 14014  !cfa 14220
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-sep 5295  ax-nul 5302  ax-pow 5359  ax-pr 5423  ax-un 7712  ax-cnex 11153  ax-resscn 11154  ax-1cn 11155  ax-icn 11156  ax-addcl 11157  ax-addrcl 11158  ax-mulcl 11159  ax-mulrcl 11160  ax-mulcom 11161  ax-addass 11162  ax-mulass 11163  ax-distr 11164  ax-i2m1 11165  ax-1ne0 11166  ax-1rid 11167  ax-rnegex 11168  ax-rrecex 11169  ax-cnre 11170  ax-pre-lttri 11171  ax-pre-lttrn 11172  ax-pre-ltadd 11173  ax-pre-mulgt0 11174
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 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3965  df-nul 4321  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4905  df-iun 4995  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  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 6292  df-ord 6359  df-on 6360  df-lim 6361  df-suc 6362  df-iota 6487  df-fun 6537  df-fn 6538  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542  df-fv 6543  df-riota 7352  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7843  df-2nd 7963  df-frecs 8253  df-wrecs 8284  df-recs 8358  df-rdg 8397  df-er 8691  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11237  df-mnf 11238  df-xr 11239  df-ltxr 11240  df-le 11241  df-sub 11433  df-neg 11434  df-div 11859  df-nn 12200  df-2 12262  df-n0 12460  df-z 12546  df-uz 12810  df-rp 12962  df-ioc 13316  df-seq 13954  df-exp 14015  df-fac 14221
This theorem is referenced by:  aaliou3lem3  25826
  Copyright terms: Public domain W3C validator