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

Theorem aaliou3lem2 25031
 Description: Lemma for aaliou3 25039. (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 12351 . . . . 5 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → 𝐵 ∈ ℕ)
2 fveq2 6659 . . . . . . . 8 (𝑎 = 𝐵 → (!‘𝑎) = (!‘𝐵))
32negeqd 10911 . . . . . . 7 (𝑎 = 𝐵 → -(!‘𝑎) = -(!‘𝐵))
43oveq2d 7167 . . . . . 6 (𝑎 = 𝐵 → (2↑-(!‘𝑎)) = (2↑-(!‘𝐵)))
5 aaliou3lem.b . . . . . 6 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))
6 ovex 7184 . . . . . 6 (2↑-(!‘𝐵)) ∈ V
74, 5, 6fvmpt 6760 . . . . 5 (𝐵 ∈ ℕ → (𝐹𝐵) = (2↑-(!‘𝐵)))
81, 7syl 17 . . . 4 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → (𝐹𝐵) = (2↑-(!‘𝐵)))
9 2rp 12428 . . . . 5 2 ∈ ℝ+
101nnnn0d 11987 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → 𝐵 ∈ ℕ0)
1110faccld 13687 . . . . . . 7 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → (!‘𝐵) ∈ ℕ)
1211nnzd 12118 . . . . . 6 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → (!‘𝐵) ∈ ℤ)
1312znegcld 12121 . . . . 5 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → -(!‘𝐵) ∈ ℤ)
14 rpexpcl 13491 . . . . 5 ((2 ∈ ℝ+ ∧ -(!‘𝐵) ∈ ℤ) → (2↑-(!‘𝐵)) ∈ ℝ+)
159, 13, 14sylancr 591 . . . 4 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → (2↑-(!‘𝐵)) ∈ ℝ+)
168, 15eqeltrd 2853 . . 3 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → (𝐹𝐵) ∈ ℝ+)
1716rpred 12465 . 2 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → (𝐹𝐵) ∈ ℝ)
1816rpgt0d 12468 . 2 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → 0 < (𝐹𝐵))
19 fveq2 6659 . . . . . 6 (𝑏 = 𝐴 → (𝐹𝑏) = (𝐹𝐴))
20 fveq2 6659 . . . . . 6 (𝑏 = 𝐴 → (𝐺𝑏) = (𝐺𝐴))
2119, 20breq12d 5046 . . . . 5 (𝑏 = 𝐴 → ((𝐹𝑏) ≤ (𝐺𝑏) ↔ (𝐹𝐴) ≤ (𝐺𝐴)))
2221imbi2d 345 . . . 4 (𝑏 = 𝐴 → ((𝐴 ∈ ℕ → (𝐹𝑏) ≤ (𝐺𝑏)) ↔ (𝐴 ∈ ℕ → (𝐹𝐴) ≤ (𝐺𝐴))))
23 fveq2 6659 . . . . . 6 (𝑏 = 𝑑 → (𝐹𝑏) = (𝐹𝑑))
24 fveq2 6659 . . . . . 6 (𝑏 = 𝑑 → (𝐺𝑏) = (𝐺𝑑))
2523, 24breq12d 5046 . . . . 5 (𝑏 = 𝑑 → ((𝐹𝑏) ≤ (𝐺𝑏) ↔ (𝐹𝑑) ≤ (𝐺𝑑)))
2625imbi2d 345 . . . 4 (𝑏 = 𝑑 → ((𝐴 ∈ ℕ → (𝐹𝑏) ≤ (𝐺𝑏)) ↔ (𝐴 ∈ ℕ → (𝐹𝑑) ≤ (𝐺𝑑))))
27 fveq2 6659 . . . . . 6 (𝑏 = (𝑑 + 1) → (𝐹𝑏) = (𝐹‘(𝑑 + 1)))
28 fveq2 6659 . . . . . 6 (𝑏 = (𝑑 + 1) → (𝐺𝑏) = (𝐺‘(𝑑 + 1)))
2927, 28breq12d 5046 . . . . 5 (𝑏 = (𝑑 + 1) → ((𝐹𝑏) ≤ (𝐺𝑏) ↔ (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1))))
3029imbi2d 345 . . . 4 (𝑏 = (𝑑 + 1) → ((𝐴 ∈ ℕ → (𝐹𝑏) ≤ (𝐺𝑏)) ↔ (𝐴 ∈ ℕ → (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1)))))
31 fveq2 6659 . . . . . 6 (𝑏 = 𝐵 → (𝐹𝑏) = (𝐹𝐵))
32 fveq2 6659 . . . . . 6 (𝑏 = 𝐵 → (𝐺𝑏) = (𝐺𝐵))
3331, 32breq12d 5046 . . . . 5 (𝑏 = 𝐵 → ((𝐹𝑏) ≤ (𝐺𝑏) ↔ (𝐹𝐵) ≤ (𝐺𝐵)))
3433imbi2d 345 . . . 4 (𝑏 = 𝐵 → ((𝐴 ∈ ℕ → (𝐹𝑏) ≤ (𝐺𝑏)) ↔ (𝐴 ∈ ℕ → (𝐹𝐵) ≤ (𝐺𝐵))))
35 nnnn0 11934 . . . . . . . . . . . 12 (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)
3635faccld 13687 . . . . . . . . . . 11 (𝐴 ∈ ℕ → (!‘𝐴) ∈ ℕ)
3736nnzd 12118 . . . . . . . . . 10 (𝐴 ∈ ℕ → (!‘𝐴) ∈ ℤ)
3837znegcld 12121 . . . . . . . . 9 (𝐴 ∈ ℕ → -(!‘𝐴) ∈ ℤ)
39 rpexpcl 13491 . . . . . . . . 9 ((2 ∈ ℝ+ ∧ -(!‘𝐴) ∈ ℤ) → (2↑-(!‘𝐴)) ∈ ℝ+)
409, 38, 39sylancr 591 . . . . . . . 8 (𝐴 ∈ ℕ → (2↑-(!‘𝐴)) ∈ ℝ+)
4140rpred 12465 . . . . . . 7 (𝐴 ∈ ℕ → (2↑-(!‘𝐴)) ∈ ℝ)
4241leidd 11237 . . . . . 6 (𝐴 ∈ ℕ → (2↑-(!‘𝐴)) ≤ (2↑-(!‘𝐴)))
43 nncn 11675 . . . . . . . . . . 11 (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
4443subidd 11016 . . . . . . . . . 10 (𝐴 ∈ ℕ → (𝐴𝐴) = 0)
4544oveq2d 7167 . . . . . . . . 9 (𝐴 ∈ ℕ → ((1 / 2)↑(𝐴𝐴)) = ((1 / 2)↑0))
46 halfcn 11882 . . . . . . . . . 10 (1 / 2) ∈ ℂ
47 exp0 13476 . . . . . . . . . 10 ((1 / 2) ∈ ℂ → ((1 / 2)↑0) = 1)
4846, 47ax-mp 5 . . . . . . . . 9 ((1 / 2)↑0) = 1
4945, 48eqtrdi 2810 . . . . . . . 8 (𝐴 ∈ ℕ → ((1 / 2)↑(𝐴𝐴)) = 1)
5049oveq2d 7167 . . . . . . 7 (𝐴 ∈ ℕ → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴𝐴))) = ((2↑-(!‘𝐴)) · 1))
5140rpcnd 12467 . . . . . . . 8 (𝐴 ∈ ℕ → (2↑-(!‘𝐴)) ∈ ℂ)
5251mulid1d 10689 . . . . . . 7 (𝐴 ∈ ℕ → ((2↑-(!‘𝐴)) · 1) = (2↑-(!‘𝐴)))
5350, 52eqtrd 2794 . . . . . 6 (𝐴 ∈ ℕ → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴𝐴))) = (2↑-(!‘𝐴)))
5442, 53breqtrrd 5061 . . . . 5 (𝐴 ∈ ℕ → (2↑-(!‘𝐴)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴𝐴))))
55 fveq2 6659 . . . . . . . 8 (𝑎 = 𝐴 → (!‘𝑎) = (!‘𝐴))
5655negeqd 10911 . . . . . . 7 (𝑎 = 𝐴 → -(!‘𝑎) = -(!‘𝐴))
5756oveq2d 7167 . . . . . 6 (𝑎 = 𝐴 → (2↑-(!‘𝑎)) = (2↑-(!‘𝐴)))
58 ovex 7184 . . . . . 6 (2↑-(!‘𝐴)) ∈ V
5957, 5, 58fvmpt 6760 . . . . 5 (𝐴 ∈ ℕ → (𝐹𝐴) = (2↑-(!‘𝐴)))
60 nnz 12036 . . . . . 6 (𝐴 ∈ ℕ → 𝐴 ∈ ℤ)
61 uzid 12290 . . . . . 6 (𝐴 ∈ ℤ → 𝐴 ∈ (ℤ𝐴))
62 oveq1 7158 . . . . . . . . 9 (𝑐 = 𝐴 → (𝑐𝐴) = (𝐴𝐴))
6362oveq2d 7167 . . . . . . . 8 (𝑐 = 𝐴 → ((1 / 2)↑(𝑐𝐴)) = ((1 / 2)↑(𝐴𝐴)))
6463oveq2d 7167 . . . . . . 7 (𝑐 = 𝐴 → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐𝐴))) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴𝐴))))
65 aaliou3lem.a . . . . . . 7 𝐺 = (𝑐 ∈ (ℤ𝐴) ↦ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐𝐴))))
66 ovex 7184 . . . . . . 7 ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴𝐴))) ∈ V
6764, 65, 66fvmpt 6760 . . . . . 6 (𝐴 ∈ (ℤ𝐴) → (𝐺𝐴) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴𝐴))))
6860, 61, 673syl 18 . . . . 5 (𝐴 ∈ ℕ → (𝐺𝐴) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴𝐴))))
6954, 59, 683brtr4d 5065 . . . 4 (𝐴 ∈ ℕ → (𝐹𝐴) ≤ (𝐺𝐴))
70 eluznn 12351 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 𝑑 ∈ ℕ)
7170nnnn0d 11987 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 𝑑 ∈ ℕ0)
7271faccld 13687 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (!‘𝑑) ∈ ℕ)
7372nnzd 12118 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (!‘𝑑) ∈ ℤ)
7473znegcld 12121 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → -(!‘𝑑) ∈ ℤ)
75 rpexpcl 13491 . . . . . . . . . . . . . 14 ((2 ∈ ℝ+ ∧ -(!‘𝑑) ∈ ℤ) → (2↑-(!‘𝑑)) ∈ ℝ+)
769, 74, 75sylancr 591 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑-(!‘𝑑)) ∈ ℝ+)
7776rpred 12465 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑-(!‘𝑑)) ∈ ℝ)
7876rpge0d 12469 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 0 ≤ (2↑-(!‘𝑑)))
79 simpl 487 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 𝐴 ∈ ℕ)
8079nnnn0d 11987 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 𝐴 ∈ ℕ0)
8180faccld 13687 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (!‘𝐴) ∈ ℕ)
8281nnzd 12118 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (!‘𝐴) ∈ ℤ)
8382znegcld 12121 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → -(!‘𝐴) ∈ ℤ)
849, 83, 39sylancr 591 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑-(!‘𝐴)) ∈ ℝ+)
85 halfre 11881 . . . . . . . . . . . . . . . 16 (1 / 2) ∈ ℝ
86 halfgt0 11883 . . . . . . . . . . . . . . . 16 0 < (1 / 2)
8785, 86elrpii 12426 . . . . . . . . . . . . . . 15 (1 / 2) ∈ ℝ+
88 eluzelz 12285 . . . . . . . . . . . . . . . 16 (𝑑 ∈ (ℤ𝐴) → 𝑑 ∈ ℤ)
89 zsubcl 12056 . . . . . . . . . . . . . . . 16 ((𝑑 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑑𝐴) ∈ ℤ)
9088, 60, 89syl2anr 600 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (𝑑𝐴) ∈ ℤ)
91 rpexpcl 13491 . . . . . . . . . . . . . . 15 (((1 / 2) ∈ ℝ+ ∧ (𝑑𝐴) ∈ ℤ) → ((1 / 2)↑(𝑑𝐴)) ∈ ℝ+)
9287, 90, 91sylancr 591 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((1 / 2)↑(𝑑𝐴)) ∈ ℝ+)
9384, 92rpmulcld 12481 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) ∈ ℝ+)
9493rpred 12465 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) ∈ ℝ)
9577, 78, 94jca31 519 . . . . . . . . . . 11 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (((2↑-(!‘𝑑)) ∈ ℝ ∧ 0 ≤ (2↑-(!‘𝑑))) ∧ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) ∈ ℝ))
9695adantr 485 . . . . . . . . . 10 (((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) ∧ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴)))) → (((2↑-(!‘𝑑)) ∈ ℝ ∧ 0 ≤ (2↑-(!‘𝑑))) ∧ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) ∈ ℝ))
9788adantl 486 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 𝑑 ∈ ℤ)
9874, 97zmulcld 12125 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (-(!‘𝑑) · 𝑑) ∈ ℤ)
99 rpexpcl 13491 . . . . . . . . . . . . . 14 ((2 ∈ ℝ+ ∧ (-(!‘𝑑) · 𝑑) ∈ ℤ) → (2↑(-(!‘𝑑) · 𝑑)) ∈ ℝ+)
1009, 98, 99sylancr 591 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑(-(!‘𝑑) · 𝑑)) ∈ ℝ+)
101100rpred 12465 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑(-(!‘𝑑) · 𝑑)) ∈ ℝ)
102100rpge0d 12469 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 0 ≤ (2↑(-(!‘𝑑) · 𝑑)))
10385a1i 11 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (1 / 2) ∈ ℝ)
104101, 102, 103jca31 519 . . . . . . . . . . 11 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (((2↑(-(!‘𝑑) · 𝑑)) ∈ ℝ ∧ 0 ≤ (2↑(-(!‘𝑑) · 𝑑))) ∧ (1 / 2) ∈ ℝ))
105104adantr 485 . . . . . . . . . 10 (((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) ∧ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴)))) → (((2↑(-(!‘𝑑) · 𝑑)) ∈ ℝ ∧ 0 ≤ (2↑(-(!‘𝑑) · 𝑑))) ∧ (1 / 2) ∈ ℝ))
106 simpr 489 . . . . . . . . . 10 (((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) ∧ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴)))) → (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))))
107 2re 11741 . . . . . . . . . . . . 13 2 ∈ ℝ
108 1le2 11876 . . . . . . . . . . . . 13 1 ≤ 2
10972nncnd 11683 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (!‘𝑑) ∈ ℂ)
11097zcnd 12120 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 𝑑 ∈ ℂ)
111109, 110mulneg1d 11124 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (-(!‘𝑑) · 𝑑) = -((!‘𝑑) · 𝑑))
11272, 70nnmulcld 11720 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((!‘𝑑) · 𝑑) ∈ ℕ)
113112nnge1d 11715 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 1 ≤ ((!‘𝑑) · 𝑑))
114 1re 10672 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
115112nnred 11682 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((!‘𝑑) · 𝑑) ∈ ℝ)
116 leneg 11174 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ ((!‘𝑑) · 𝑑) ∈ ℝ) → (1 ≤ ((!‘𝑑) · 𝑑) ↔ -((!‘𝑑) · 𝑑) ≤ -1))
117114, 115, 116sylancr 591 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (1 ≤ ((!‘𝑑) · 𝑑) ↔ -((!‘𝑑) · 𝑑) ≤ -1))
118113, 117mpbid 235 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → -((!‘𝑑) · 𝑑) ≤ -1)
119111, 118eqbrtrd 5055 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (-(!‘𝑑) · 𝑑) ≤ -1)
120 neg1z 12050 . . . . . . . . . . . . . . 15 -1 ∈ ℤ
121 eluz 12289 . . . . . . . . . . . . . . 15 (((-(!‘𝑑) · 𝑑) ∈ ℤ ∧ -1 ∈ ℤ) → (-1 ∈ (ℤ‘(-(!‘𝑑) · 𝑑)) ↔ (-(!‘𝑑) · 𝑑) ≤ -1))
12298, 120, 121sylancl 590 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (-1 ∈ (ℤ‘(-(!‘𝑑) · 𝑑)) ↔ (-(!‘𝑑) · 𝑑) ≤ -1))
123119, 122mpbird 260 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → -1 ∈ (ℤ‘(-(!‘𝑑) · 𝑑)))
124 leexp2a 13579 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ 1 ≤ 2 ∧ -1 ∈ (ℤ‘(-(!‘𝑑) · 𝑑))) → (2↑(-(!‘𝑑) · 𝑑)) ≤ (2↑-1))
125107, 108, 123, 124mp3an12i 1463 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑(-(!‘𝑑) · 𝑑)) ≤ (2↑-1))
126 2cn 11742 . . . . . . . . . . . . 13 2 ∈ ℂ
127 expn1 13482 . . . . . . . . . . . . 13 (2 ∈ ℂ → (2↑-1) = (1 / 2))
128126, 127ax-mp 5 . . . . . . . . . . . 12 (2↑-1) = (1 / 2)
129125, 128breqtrdi 5074 . . . . . . . . . . 11 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑(-(!‘𝑑) · 𝑑)) ≤ (1 / 2))
130129adantr 485 . . . . . . . . . 10 (((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) ∧ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴)))) → (2↑(-(!‘𝑑) · 𝑑)) ≤ (1 / 2))
131 lemul12a 11529 . . . . . . . . . . 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 1115 . . . . . . . . . 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 1372 . . . . . . . . 9 (((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) ∧ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴)))) → ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))) ≤ (((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) · (1 / 2)))
134133ex 417 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) → ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))) ≤ (((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) · (1 / 2))))
135 facp1 13681 . . . . . . . . . . . . . 14 (𝑑 ∈ ℕ0 → (!‘(𝑑 + 1)) = ((!‘𝑑) · (𝑑 + 1)))
13671, 135syl 17 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (!‘(𝑑 + 1)) = ((!‘𝑑) · (𝑑 + 1)))
137136negeqd 10911 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → -(!‘(𝑑 + 1)) = -((!‘𝑑) · (𝑑 + 1)))
138 ax-1cn 10626 . . . . . . . . . . . . . . 15 1 ∈ ℂ
139 addcom 10857 . . . . . . . . . . . . . . 15 ((𝑑 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑑 + 1) = (1 + 𝑑))
140110, 138, 139sylancl 590 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (𝑑 + 1) = (1 + 𝑑))
141140oveq2d 7167 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (-(!‘𝑑) · (𝑑 + 1)) = (-(!‘𝑑) · (1 + 𝑑)))
142 peano2cn 10843 . . . . . . . . . . . . . . 15 (𝑑 ∈ ℂ → (𝑑 + 1) ∈ ℂ)
143110, 142syl 17 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (𝑑 + 1) ∈ ℂ)
144109, 143mulneg1d 11124 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (-(!‘𝑑) · (𝑑 + 1)) = -((!‘𝑑) · (𝑑 + 1)))
14574zcnd 12120 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → -(!‘𝑑) ∈ ℂ)
146 1cnd 10667 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 1 ∈ ℂ)
147145, 146, 110adddid 10696 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (-(!‘𝑑) · (1 + 𝑑)) = ((-(!‘𝑑) · 1) + (-(!‘𝑑) · 𝑑)))
148145mulid1d 10689 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (-(!‘𝑑) · 1) = -(!‘𝑑))
149148oveq1d 7166 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((-(!‘𝑑) · 1) + (-(!‘𝑑) · 𝑑)) = (-(!‘𝑑) + (-(!‘𝑑) · 𝑑)))
150147, 149eqtrd 2794 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (-(!‘𝑑) · (1 + 𝑑)) = (-(!‘𝑑) + (-(!‘𝑑) · 𝑑)))
151141, 144, 1503eqtr3d 2802 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → -((!‘𝑑) · (𝑑 + 1)) = (-(!‘𝑑) + (-(!‘𝑑) · 𝑑)))
152137, 151eqtrd 2794 . . . . . . . . . . 11 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → -(!‘(𝑑 + 1)) = (-(!‘𝑑) + (-(!‘𝑑) · 𝑑)))
153152oveq2d 7167 . . . . . . . . . 10 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑-(!‘(𝑑 + 1))) = (2↑(-(!‘𝑑) + (-(!‘𝑑) · 𝑑))))
154 2cnne0 11877 . . . . . . . . . . . 12 (2 ∈ ℂ ∧ 2 ≠ 0)
155 expaddz 13516 . . . . . . . . . . . 12 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (-(!‘𝑑) ∈ ℤ ∧ (-(!‘𝑑) · 𝑑) ∈ ℤ)) → (2↑(-(!‘𝑑) + (-(!‘𝑑) · 𝑑))) = ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))))
156154, 155mpan 690 . . . . . . . . . . 11 ((-(!‘𝑑) ∈ ℤ ∧ (-(!‘𝑑) · 𝑑) ∈ ℤ) → (2↑(-(!‘𝑑) + (-(!‘𝑑) · 𝑑))) = ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))))
15774, 98, 156syl2anc 588 . . . . . . . . . 10 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑(-(!‘𝑑) + (-(!‘𝑑) · 𝑑))) = ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))))
158153, 157eqtrd 2794 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑-(!‘(𝑑 + 1))) = ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))))
15943adantr 485 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → 𝐴 ∈ ℂ)
160110, 146, 159addsubd 11049 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((𝑑 + 1) − 𝐴) = ((𝑑𝐴) + 1))
161160oveq2d 7167 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((1 / 2)↑((𝑑 + 1) − 𝐴)) = ((1 / 2)↑((𝑑𝐴) + 1)))
162 uznn0sub 12310 . . . . . . . . . . . . . 14 (𝑑 ∈ (ℤ𝐴) → (𝑑𝐴) ∈ ℕ0)
163162adantl 486 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (𝑑𝐴) ∈ ℕ0)
164 expp1 13479 . . . . . . . . . . . . 13 (((1 / 2) ∈ ℂ ∧ (𝑑𝐴) ∈ ℕ0) → ((1 / 2)↑((𝑑𝐴) + 1)) = (((1 / 2)↑(𝑑𝐴)) · (1 / 2)))
16546, 163, 164sylancr 591 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((1 / 2)↑((𝑑𝐴) + 1)) = (((1 / 2)↑(𝑑𝐴)) · (1 / 2)))
166161, 165eqtrd 2794 . . . . . . . . . . 11 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((1 / 2)↑((𝑑 + 1) − 𝐴)) = (((1 / 2)↑(𝑑𝐴)) · (1 / 2)))
167166oveq2d 7167 . . . . . . . . . 10 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))) = ((2↑-(!‘𝐴)) · (((1 / 2)↑(𝑑𝐴)) · (1 / 2))))
16884rpcnd 12467 . . . . . . . . . . 11 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (2↑-(!‘𝐴)) ∈ ℂ)
16992rpcnd 12467 . . . . . . . . . . 11 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((1 / 2)↑(𝑑𝐴)) ∈ ℂ)
17046a1i 11 . . . . . . . . . . 11 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (1 / 2) ∈ ℂ)
171168, 169, 170mulassd 10695 . . . . . . . . . 10 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) · (1 / 2)) = ((2↑-(!‘𝐴)) · (((1 / 2)↑(𝑑𝐴)) · (1 / 2))))
172167, 171eqtr4d 2797 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))) = (((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) · (1 / 2)))
173158, 172breq12d 5046 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((2↑-(!‘(𝑑 + 1))) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))) ↔ ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))) ≤ (((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) · (1 / 2))))
174134, 173sylibrd 262 . . . . . . 7 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) → (2↑-(!‘(𝑑 + 1))) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴)))))
175 fveq2 6659 . . . . . . . . . . . 12 (𝑎 = 𝑑 → (!‘𝑎) = (!‘𝑑))
176175negeqd 10911 . . . . . . . . . . 11 (𝑎 = 𝑑 → -(!‘𝑎) = -(!‘𝑑))
177176oveq2d 7167 . . . . . . . . . 10 (𝑎 = 𝑑 → (2↑-(!‘𝑎)) = (2↑-(!‘𝑑)))
178 ovex 7184 . . . . . . . . . 10 (2↑-(!‘𝑑)) ∈ V
179177, 5, 178fvmpt 6760 . . . . . . . . 9 (𝑑 ∈ ℕ → (𝐹𝑑) = (2↑-(!‘𝑑)))
18070, 179syl 17 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (𝐹𝑑) = (2↑-(!‘𝑑)))
181 oveq1 7158 . . . . . . . . . . . 12 (𝑐 = 𝑑 → (𝑐𝐴) = (𝑑𝐴))
182181oveq2d 7167 . . . . . . . . . . 11 (𝑐 = 𝑑 → ((1 / 2)↑(𝑐𝐴)) = ((1 / 2)↑(𝑑𝐴)))
183182oveq2d 7167 . . . . . . . . . 10 (𝑐 = 𝑑 → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐𝐴))) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))))
184 ovex 7184 . . . . . . . . . 10 ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))) ∈ V
185183, 65, 184fvmpt 6760 . . . . . . . . 9 (𝑑 ∈ (ℤ𝐴) → (𝐺𝑑) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))))
186185adantl 486 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (𝐺𝑑) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴))))
187180, 186breq12d 5046 . . . . . . 7 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((𝐹𝑑) ≤ (𝐺𝑑) ↔ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑𝐴)))))
18870peano2nnd 11684 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (𝑑 + 1) ∈ ℕ)
189 fveq2 6659 . . . . . . . . . . . 12 (𝑎 = (𝑑 + 1) → (!‘𝑎) = (!‘(𝑑 + 1)))
190189negeqd 10911 . . . . . . . . . . 11 (𝑎 = (𝑑 + 1) → -(!‘𝑎) = -(!‘(𝑑 + 1)))
191190oveq2d 7167 . . . . . . . . . 10 (𝑎 = (𝑑 + 1) → (2↑-(!‘𝑎)) = (2↑-(!‘(𝑑 + 1))))
192 ovex 7184 . . . . . . . . . 10 (2↑-(!‘(𝑑 + 1))) ∈ V
193191, 5, 192fvmpt 6760 . . . . . . . . 9 ((𝑑 + 1) ∈ ℕ → (𝐹‘(𝑑 + 1)) = (2↑-(!‘(𝑑 + 1))))
194188, 193syl 17 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (𝐹‘(𝑑 + 1)) = (2↑-(!‘(𝑑 + 1))))
195 peano2uz 12334 . . . . . . . . . 10 (𝑑 ∈ (ℤ𝐴) → (𝑑 + 1) ∈ (ℤ𝐴))
196 oveq1 7158 . . . . . . . . . . . . 13 (𝑐 = (𝑑 + 1) → (𝑐𝐴) = ((𝑑 + 1) − 𝐴))
197196oveq2d 7167 . . . . . . . . . . . 12 (𝑐 = (𝑑 + 1) → ((1 / 2)↑(𝑐𝐴)) = ((1 / 2)↑((𝑑 + 1) − 𝐴)))
198197oveq2d 7167 . . . . . . . . . . 11 (𝑐 = (𝑑 + 1) → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐𝐴))) = ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))))
199 ovex 7184 . . . . . . . . . . 11 ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))) ∈ V
200198, 65, 199fvmpt 6760 . . . . . . . . . 10 ((𝑑 + 1) ∈ (ℤ𝐴) → (𝐺‘(𝑑 + 1)) = ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))))
201195, 200syl 17 . . . . . . . . 9 (𝑑 ∈ (ℤ𝐴) → (𝐺‘(𝑑 + 1)) = ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))))
202201adantl 486 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → (𝐺‘(𝑑 + 1)) = ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))))
203194, 202breq12d 5046 . . . . . . 7 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1)) ↔ (2↑-(!‘(𝑑 + 1))) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴)))))
204174, 187, 2033imtr4d 298 . . . . . 6 ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ𝐴)) → ((𝐹𝑑) ≤ (𝐺𝑑) → (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1))))
205204expcom 418 . . . . 5 (𝑑 ∈ (ℤ𝐴) → (𝐴 ∈ ℕ → ((𝐹𝑑) ≤ (𝐺𝑑) → (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1)))))
206205a2d 29 . . . 4 (𝑑 ∈ (ℤ𝐴) → ((𝐴 ∈ ℕ → (𝐹𝑑) ≤ (𝐺𝑑)) → (𝐴 ∈ ℕ → (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1)))))
20722, 26, 30, 34, 69, 206uzind4i 12343 . . 3 (𝐵 ∈ (ℤ𝐴) → (𝐴 ∈ ℕ → (𝐹𝐵) ≤ (𝐺𝐵)))
208207impcom 412 . 2 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → (𝐹𝐵) ≤ (𝐺𝐵))
209 0xr 10719 . . 3 0 ∈ ℝ*
21065aaliou3lem1 25030 . . 3 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → (𝐺𝐵) ∈ ℝ)
211 elioc2 12835 . . 3 ((0 ∈ ℝ* ∧ (𝐺𝐵) ∈ ℝ) → ((𝐹𝐵) ∈ (0(,](𝐺𝐵)) ↔ ((𝐹𝐵) ∈ ℝ ∧ 0 < (𝐹𝐵) ∧ (𝐹𝐵) ≤ (𝐺𝐵))))
212209, 210, 211sylancr 591 . 2 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → ((𝐹𝐵) ∈ (0(,](𝐺𝐵)) ↔ ((𝐹𝐵) ∈ ℝ ∧ 0 < (𝐹𝐵) ∧ (𝐹𝐵) ≤ (𝐺𝐵))))
21317, 18, 208, 212mpbir3and 1340 1 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ𝐴)) → (𝐹𝐵) ∈ (0(,](𝐺𝐵)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112   ≠ wne 2952   class class class wbr 5033   ↦ cmpt 5113  ‘cfv 6336  (class class class)co 7151  ℂcc 10566  ℝcr 10567  0cc0 10568  1c1 10569   + caddc 10571   · cmul 10573  ℝ*cxr 10705   < clt 10706   ≤ cle 10707   − cmin 10901  -cneg 10902   / cdiv 11328  ℕcn 11667  2c2 11722  ℕ0cn0 11927  ℤcz 12013  ℤ≥cuz 12275  ℝ+crp 12423  (,]cioc 12773  ↑cexp 13472  !cfa 13676 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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-cnex 10624  ax-resscn 10625  ax-1cn 10626  ax-icn 10627  ax-addcl 10628  ax-addrcl 10629  ax-mulcl 10630  ax-mulrcl 10631  ax-mulcom 10632  ax-addass 10633  ax-mulass 10634  ax-distr 10635  ax-i2m1 10636  ax-1ne0 10637  ax-1rid 10638  ax-rnegex 10639  ax-rrecex 10640  ax-cnre 10641  ax-pre-lttri 10642  ax-pre-lttrn 10643  ax-pre-ltadd 10644  ax-pre-mulgt0 10645 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7581  df-2nd 7695  df-wrecs 7958  df-recs 8019  df-rdg 8057  df-er 8300  df-en 8529  df-dom 8530  df-sdom 8531  df-pnf 10708  df-mnf 10709  df-xr 10710  df-ltxr 10711  df-le 10712  df-sub 10903  df-neg 10904  df-div 11329  df-nn 11668  df-2 11730  df-n0 11928  df-z 12014  df-uz 12276  df-rp 12424  df-ioc 12777  df-seq 13412  df-exp 13473  df-fac 13677 This theorem is referenced by:  aaliou3lem3  25032
 Copyright terms: Public domain W3C validator