Theorem aaliou3lem2 25863

Description: Lemma for aaliou3 25871. (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.

Step	Hyp	Ref	Expression
1		eluznn 12904	. . . . 5 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → 𝐵 ∈ ℕ)
2		fveq2 6891	. . . . . . . 8 ⊢ (𝑎 = 𝐵 → (!‘𝑎) = (!‘𝐵))
3	2	negeqd 11456	. . . . . . 7 ⊢ (𝑎 = 𝐵 → -(!‘𝑎) = -(!‘𝐵))
4	3	oveq2d 7427	. . . . . 6 ⊢ (𝑎 = 𝐵 → (2↑-(!‘𝑎)) = (2↑-(!‘𝐵)))
5		aaliou3lem.b	. . . . . 6 ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))
6		ovex 7444	. . . . . 6 ⊢ (2↑-(!‘𝐵)) ∈ V
7	4, 5, 6	fvmpt 6998	. . . . 5 ⊢ (𝐵 ∈ ℕ → (𝐹‘𝐵) = (2↑-(!‘𝐵)))
8	1, 7	syl 17	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐹‘𝐵) = (2↑-(!‘𝐵)))
9		2rp 12981	. . . . 5 ⊢ 2 ∈ ℝ+
10	1	nnnn0d 12534	. . . . . . . 8 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → 𝐵 ∈ ℕ0)
11	10	faccld 14246	. . . . . . 7 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (!‘𝐵) ∈ ℕ)
12	11	nnzd 12587	. . . . . 6 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (!‘𝐵) ∈ ℤ)
13	12	znegcld 12670	. . . . 5 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → -(!‘𝐵) ∈ ℤ)
14		rpexpcl 14048	. . . . 5 ⊢ ((2 ∈ ℝ+ ∧ -(!‘𝐵) ∈ ℤ) → (2↑-(!‘𝐵)) ∈ ℝ+)
15	9, 13, 14	sylancr 587	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (2↑-(!‘𝐵)) ∈ ℝ+)
16	8, 15	eqeltrd 2833	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐹‘𝐵) ∈ ℝ+)
17	16	rpred 13018	. 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐹‘𝐵) ∈ ℝ)
18	16	rpgt0d 13021	. 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → 0 < (𝐹‘𝐵))
19		fveq2 6891	. . . . . 6 ⊢ (𝑏 = 𝐴 → (𝐹‘𝑏) = (𝐹‘𝐴))
20		fveq2 6891	. . . . . 6 ⊢ (𝑏 = 𝐴 → (𝐺‘𝑏) = (𝐺‘𝐴))
21	19, 20	breq12d 5161	. . . . 5 ⊢ (𝑏 = 𝐴 → ((𝐹‘𝑏) ≤ (𝐺‘𝑏) ↔ (𝐹‘𝐴) ≤ (𝐺‘𝐴)))
22	21	imbi2d 340	. . . 4 ⊢ (𝑏 = 𝐴 → ((𝐴 ∈ ℕ → (𝐹‘𝑏) ≤ (𝐺‘𝑏)) ↔ (𝐴 ∈ ℕ → (𝐹‘𝐴) ≤ (𝐺‘𝐴))))
23		fveq2 6891	. . . . . 6 ⊢ (𝑏 = 𝑑 → (𝐹‘𝑏) = (𝐹‘𝑑))
24		fveq2 6891	. . . . . 6 ⊢ (𝑏 = 𝑑 → (𝐺‘𝑏) = (𝐺‘𝑑))
25	23, 24	breq12d 5161	. . . . 5 ⊢ (𝑏 = 𝑑 → ((𝐹‘𝑏) ≤ (𝐺‘𝑏) ↔ (𝐹‘𝑑) ≤ (𝐺‘𝑑)))
26	25	imbi2d 340	. . . 4 ⊢ (𝑏 = 𝑑 → ((𝐴 ∈ ℕ → (𝐹‘𝑏) ≤ (𝐺‘𝑏)) ↔ (𝐴 ∈ ℕ → (𝐹‘𝑑) ≤ (𝐺‘𝑑))))
27		fveq2 6891	. . . . . 6 ⊢ (𝑏 = (𝑑 + 1) → (𝐹‘𝑏) = (𝐹‘(𝑑 + 1)))
28		fveq2 6891	. . . . . 6 ⊢ (𝑏 = (𝑑 + 1) → (𝐺‘𝑏) = (𝐺‘(𝑑 + 1)))
29	27, 28	breq12d 5161	. . . . 5 ⊢ (𝑏 = (𝑑 + 1) → ((𝐹‘𝑏) ≤ (𝐺‘𝑏) ↔ (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1))))
30	29	imbi2d 340	. . . 4 ⊢ (𝑏 = (𝑑 + 1) → ((𝐴 ∈ ℕ → (𝐹‘𝑏) ≤ (𝐺‘𝑏)) ↔ (𝐴 ∈ ℕ → (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1)))))
31		fveq2 6891	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝐹‘𝑏) = (𝐹‘𝐵))
32		fveq2 6891	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝐺‘𝑏) = (𝐺‘𝐵))
33	31, 32	breq12d 5161	. . . . 5 ⊢ (𝑏 = 𝐵 → ((𝐹‘𝑏) ≤ (𝐺‘𝑏) ↔ (𝐹‘𝐵) ≤ (𝐺‘𝐵)))
34	33	imbi2d 340	. . . 4 ⊢ (𝑏 = 𝐵 → ((𝐴 ∈ ℕ → (𝐹‘𝑏) ≤ (𝐺‘𝑏)) ↔ (𝐴 ∈ ℕ → (𝐹‘𝐵) ≤ (𝐺‘𝐵))))
35		nnnn0 12481	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)
36	35	faccld 14246	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℕ → (!‘𝐴) ∈ ℕ)
37	36	nnzd 12587	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℕ → (!‘𝐴) ∈ ℤ)
38	37	znegcld 12670	. . . . . . . . 9 ⊢ (𝐴 ∈ ℕ → -(!‘𝐴) ∈ ℤ)
39		rpexpcl 14048	. . . . . . . . 9 ⊢ ((2 ∈ ℝ+ ∧ -(!‘𝐴) ∈ ℤ) → (2↑-(!‘𝐴)) ∈ ℝ+)
40	9, 38, 39	sylancr 587	. . . . . . . 8 ⊢ (𝐴 ∈ ℕ → (2↑-(!‘𝐴)) ∈ ℝ+)
41	40	rpred 13018	. . . . . . 7 ⊢ (𝐴 ∈ ℕ → (2↑-(!‘𝐴)) ∈ ℝ)
42	41	leidd 11782	. . . . . 6 ⊢ (𝐴 ∈ ℕ → (2↑-(!‘𝐴)) ≤ (2↑-(!‘𝐴)))
43		nncn 12222	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
44	43	subidd 11561	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℕ → (𝐴 − 𝐴) = 0)
45	44	oveq2d 7427	. . . . . . . . 9 ⊢ (𝐴 ∈ ℕ → ((1 / 2)↑(𝐴 − 𝐴)) = ((1 / 2)↑0))
46		halfcn 12429	. . . . . . . . . 10 ⊢ (1 / 2) ∈ ℂ
47		exp0 14033	. . . . . . . . . 10 ⊢ ((1 / 2) ∈ ℂ → ((1 / 2)↑0) = 1)
48	46, 47	ax-mp 5	. . . . . . . . 9 ⊢ ((1 / 2)↑0) = 1
49	45, 48	eqtrdi 2788	. . . . . . . 8 ⊢ (𝐴 ∈ ℕ → ((1 / 2)↑(𝐴 − 𝐴)) = 1)
50	49	oveq2d 7427	. . . . . . 7 ⊢ (𝐴 ∈ ℕ → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴 − 𝐴))) = ((2↑-(!‘𝐴)) · 1))
51	40	rpcnd 13020	. . . . . . . 8 ⊢ (𝐴 ∈ ℕ → (2↑-(!‘𝐴)) ∈ ℂ)
52	51	mulridd 11233	. . . . . . 7 ⊢ (𝐴 ∈ ℕ → ((2↑-(!‘𝐴)) · 1) = (2↑-(!‘𝐴)))
53	50, 52	eqtrd 2772	. . . . . 6 ⊢ (𝐴 ∈ ℕ → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴 − 𝐴))) = (2↑-(!‘𝐴)))
54	42, 53	breqtrrd 5176	. . . . 5 ⊢ (𝐴 ∈ ℕ → (2↑-(!‘𝐴)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴 − 𝐴))))
55		fveq2 6891	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → (!‘𝑎) = (!‘𝐴))
56	55	negeqd 11456	. . . . . . 7 ⊢ (𝑎 = 𝐴 → -(!‘𝑎) = -(!‘𝐴))
57	56	oveq2d 7427	. . . . . 6 ⊢ (𝑎 = 𝐴 → (2↑-(!‘𝑎)) = (2↑-(!‘𝐴)))
58		ovex 7444	. . . . . 6 ⊢ (2↑-(!‘𝐴)) ∈ V
59	57, 5, 58	fvmpt 6998	. . . . 5 ⊢ (𝐴 ∈ ℕ → (𝐹‘𝐴) = (2↑-(!‘𝐴)))
60		nnz 12581	. . . . . 6 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℤ)
61		uzid 12839	. . . . . 6 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ (ℤ≥‘𝐴))
62		oveq1 7418	. . . . . . . . 9 ⊢ (𝑐 = 𝐴 → (𝑐 − 𝐴) = (𝐴 − 𝐴))
63	62	oveq2d 7427	. . . . . . . 8 ⊢ (𝑐 = 𝐴 → ((1 / 2)↑(𝑐 − 𝐴)) = ((1 / 2)↑(𝐴 − 𝐴)))
64	63	oveq2d 7427	. . . . . . 7 ⊢ (𝑐 = 𝐴 → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴))) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴 − 𝐴))))
65		aaliou3lem.a	. . . . . . 7 ⊢ 𝐺 = (𝑐 ∈ (ℤ≥‘𝐴) ↦ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴))))
66		ovex 7444	. . . . . . 7 ⊢ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴 − 𝐴))) ∈ V
67	64, 65, 66	fvmpt 6998	. . . . . 6 ⊢ (𝐴 ∈ (ℤ≥‘𝐴) → (𝐺‘𝐴) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴 − 𝐴))))
68	60, 61, 67	3syl 18	. . . . 5 ⊢ (𝐴 ∈ ℕ → (𝐺‘𝐴) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝐴 − 𝐴))))
69	54, 59, 68	3brtr4d 5180	. . . 4 ⊢ (𝐴 ∈ ℕ → (𝐹‘𝐴) ≤ (𝐺‘𝐴))
70		eluznn 12904	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → 𝑑 ∈ ℕ)
71	70	nnnn0d 12534	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → 𝑑 ∈ ℕ0)
72	71	faccld 14246	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (!‘𝑑) ∈ ℕ)
73	72	nnzd 12587	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (!‘𝑑) ∈ ℤ)
74	73	znegcld 12670	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → -(!‘𝑑) ∈ ℤ)
75		rpexpcl 14048	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ+ ∧ -(!‘𝑑) ∈ ℤ) → (2↑-(!‘𝑑)) ∈ ℝ+)
76	9, 74, 75	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (2↑-(!‘𝑑)) ∈ ℝ+)
77	76	rpred 13018	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (2↑-(!‘𝑑)) ∈ ℝ)
78	76	rpge0d 13022	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → 0 ≤ (2↑-(!‘𝑑)))
79		simpl 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → 𝐴 ∈ ℕ)
80	79	nnnn0d 12534	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → 𝐴 ∈ ℕ0)
81	80	faccld 14246	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (!‘𝐴) ∈ ℕ)
82	81	nnzd 12587	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (!‘𝐴) ∈ ℤ)
83	82	znegcld 12670	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → -(!‘𝐴) ∈ ℤ)
84	9, 83, 39	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (2↑-(!‘𝐴)) ∈ ℝ+)
85		halfre 12428	. . . . . . . . . . . . . . . 16 ⊢ (1 / 2) ∈ ℝ
86		halfgt0 12430	. . . . . . . . . . . . . . . 16 ⊢ 0 < (1 / 2)
87	85, 86	elrpii 12979	. . . . . . . . . . . . . . 15 ⊢ (1 / 2) ∈ ℝ+
88		eluzelz 12834	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ (ℤ≥‘𝐴) → 𝑑 ∈ ℤ)
89		zsubcl 12606	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑑 − 𝐴) ∈ ℤ)
90	88, 60, 89	syl2anr 597	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (𝑑 − 𝐴) ∈ ℤ)
91		rpexpcl 14048	. . . . . . . . . . . . . . 15 ⊢ (((1 / 2) ∈ ℝ+ ∧ (𝑑 − 𝐴) ∈ ℤ) → ((1 / 2)↑(𝑑 − 𝐴)) ∈ ℝ+)
92	87, 90, 91	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → ((1 / 2)↑(𝑑 − 𝐴)) ∈ ℝ+)
93	84, 92	rpmulcld 13034	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) ∈ ℝ+)
94	93	rpred 13018	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) ∈ ℝ)
95	77, 78, 94	jca31 515	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (((2↑-(!‘𝑑)) ∈ ℝ ∧ 0 ≤ (2↑-(!‘𝑑))) ∧ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) ∈ ℝ))
96	95	adantr 481	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) ∧ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴)))) → (((2↑-(!‘𝑑)) ∈ ℝ ∧ 0 ≤ (2↑-(!‘𝑑))) ∧ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) ∈ ℝ))
97	88	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → 𝑑 ∈ ℤ)
98	74, 97	zmulcld 12674	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (-(!‘𝑑) · 𝑑) ∈ ℤ)
99		rpexpcl 14048	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ+ ∧ (-(!‘𝑑) · 𝑑) ∈ ℤ) → (2↑(-(!‘𝑑) · 𝑑)) ∈ ℝ+)
100	9, 98, 99	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (2↑(-(!‘𝑑) · 𝑑)) ∈ ℝ+)
101	100	rpred 13018	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (2↑(-(!‘𝑑) · 𝑑)) ∈ ℝ)
102	100	rpge0d 13022	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → 0 ≤ (2↑(-(!‘𝑑) · 𝑑)))
103	85	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (1 / 2) ∈ ℝ)
104	101, 102, 103	jca31 515	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (((2↑(-(!‘𝑑) · 𝑑)) ∈ ℝ ∧ 0 ≤ (2↑(-(!‘𝑑) · 𝑑))) ∧ (1 / 2) ∈ ℝ))
105	104	adantr 481	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) ∧ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴)))) → (((2↑(-(!‘𝑑) · 𝑑)) ∈ ℝ ∧ 0 ≤ (2↑(-(!‘𝑑) · 𝑑))) ∧ (1 / 2) ∈ ℝ))
106		simpr 485	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) ∧ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴)))) → (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))))
107		2re 12288	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
108		1le2 12423	. . . . . . . . . . . . 13 ⊢ 1 ≤ 2
109	72	nncnd 12230	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (!‘𝑑) ∈ ℂ)
110	97	zcnd 12669	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → 𝑑 ∈ ℂ)
111	109, 110	mulneg1d 11669	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (-(!‘𝑑) · 𝑑) = -((!‘𝑑) · 𝑑))
112	72, 70	nnmulcld 12267	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → ((!‘𝑑) · 𝑑) ∈ ℕ)
113	112	nnge1d 12262	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → 1 ≤ ((!‘𝑑) · 𝑑))
114		1re 11216	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
115	112	nnred 12229	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → ((!‘𝑑) · 𝑑) ∈ ℝ)
116		leneg 11719	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℝ ∧ ((!‘𝑑) · 𝑑) ∈ ℝ) → (1 ≤ ((!‘𝑑) · 𝑑) ↔ -((!‘𝑑) · 𝑑) ≤ -1))
117	114, 115, 116	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (1 ≤ ((!‘𝑑) · 𝑑) ↔ -((!‘𝑑) · 𝑑) ≤ -1))
118	113, 117	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → -((!‘𝑑) · 𝑑) ≤ -1)
119	111, 118	eqbrtrd 5170	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (-(!‘𝑑) · 𝑑) ≤ -1)
120		neg1z 12600	. . . . . . . . . . . . . . 15 ⊢ -1 ∈ ℤ
121		eluz 12838	. . . . . . . . . . . . . . 15 ⊢ (((-(!‘𝑑) · 𝑑) ∈ ℤ ∧ -1 ∈ ℤ) → (-1 ∈ (ℤ≥‘(-(!‘𝑑) · 𝑑)) ↔ (-(!‘𝑑) · 𝑑) ≤ -1))
122	98, 120, 121	sylancl 586	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (-1 ∈ (ℤ≥‘(-(!‘𝑑) · 𝑑)) ↔ (-(!‘𝑑) · 𝑑) ≤ -1))
123	119, 122	mpbird 256	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → -1 ∈ (ℤ≥‘(-(!‘𝑑) · 𝑑)))
124		leexp2a 14139	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ ∧ 1 ≤ 2 ∧ -1 ∈ (ℤ≥‘(-(!‘𝑑) · 𝑑))) → (2↑(-(!‘𝑑) · 𝑑)) ≤ (2↑-1))
125	107, 108, 123, 124	mp3an12i 1465	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (2↑(-(!‘𝑑) · 𝑑)) ≤ (2↑-1))
126		2cn 12289	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℂ
127		expn1 14039	. . . . . . . . . . . . 13 ⊢ (2 ∈ ℂ → (2↑-1) = (1 / 2))
128	126, 127	ax-mp 5	. . . . . . . . . . . 12 ⊢ (2↑-1) = (1 / 2)
129	125, 128	breqtrdi 5189	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (2↑(-(!‘𝑑) · 𝑑)) ≤ (1 / 2))
130	129	adantr 481	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) ∧ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴)))) → (2↑(-(!‘𝑑) · 𝑑)) ≤ (1 / 2))
131		lemul12a 12074	. . . . . . . . . . 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))))
132	131	3impia 1117	. . . . . . . . . 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)))
133	96, 105, 106, 130, 132	syl112anc 1374	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) ∧ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴)))) → ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))) ≤ (((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) · (1 / 2)))
134	133	ex 413	. . . . . . . 8 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → ((2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) → ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))) ≤ (((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) · (1 / 2))))
135		facp1 14240	. . . . . . . . . . . . . 14 ⊢ (𝑑 ∈ ℕ0 → (!‘(𝑑 + 1)) = ((!‘𝑑) · (𝑑 + 1)))
136	71, 135	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (!‘(𝑑 + 1)) = ((!‘𝑑) · (𝑑 + 1)))
137	136	negeqd 11456	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → -(!‘(𝑑 + 1)) = -((!‘𝑑) · (𝑑 + 1)))
138		ax-1cn 11170	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
139		addcom 11402	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑑 + 1) = (1 + 𝑑))
140	110, 138, 139	sylancl 586	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (𝑑 + 1) = (1 + 𝑑))
141	140	oveq2d 7427	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (-(!‘𝑑) · (𝑑 + 1)) = (-(!‘𝑑) · (1 + 𝑑)))
142		peano2cn 11388	. . . . . . . . . . . . . . 15 ⊢ (𝑑 ∈ ℂ → (𝑑 + 1) ∈ ℂ)
143	110, 142	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (𝑑 + 1) ∈ ℂ)
144	109, 143	mulneg1d 11669	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (-(!‘𝑑) · (𝑑 + 1)) = -((!‘𝑑) · (𝑑 + 1)))
145	74	zcnd 12669	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → -(!‘𝑑) ∈ ℂ)
146		1cnd 11211	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → 1 ∈ ℂ)
147	145, 146, 110	adddid 11240	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (-(!‘𝑑) · (1 + 𝑑)) = ((-(!‘𝑑) · 1) + (-(!‘𝑑) · 𝑑)))
148	145	mulridd 11233	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (-(!‘𝑑) · 1) = -(!‘𝑑))
149	148	oveq1d 7426	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → ((-(!‘𝑑) · 1) + (-(!‘𝑑) · 𝑑)) = (-(!‘𝑑) + (-(!‘𝑑) · 𝑑)))
150	147, 149	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (-(!‘𝑑) · (1 + 𝑑)) = (-(!‘𝑑) + (-(!‘𝑑) · 𝑑)))
151	141, 144, 150	3eqtr3d 2780	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → -((!‘𝑑) · (𝑑 + 1)) = (-(!‘𝑑) + (-(!‘𝑑) · 𝑑)))
152	137, 151	eqtrd 2772	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → -(!‘(𝑑 + 1)) = (-(!‘𝑑) + (-(!‘𝑑) · 𝑑)))
153	152	oveq2d 7427	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (2↑-(!‘(𝑑 + 1))) = (2↑(-(!‘𝑑) + (-(!‘𝑑) · 𝑑))))
154		2cnne0 12424	. . . . . . . . . . . 12 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
155		expaddz 14074	. . . . . . . . . . . 12 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (-(!‘𝑑) ∈ ℤ ∧ (-(!‘𝑑) · 𝑑) ∈ ℤ)) → (2↑(-(!‘𝑑) + (-(!‘𝑑) · 𝑑))) = ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))))
156	154, 155	mpan 688	. . . . . . . . . . 11 ⊢ ((-(!‘𝑑) ∈ ℤ ∧ (-(!‘𝑑) · 𝑑) ∈ ℤ) → (2↑(-(!‘𝑑) + (-(!‘𝑑) · 𝑑))) = ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))))
157	74, 98, 156	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (2↑(-(!‘𝑑) + (-(!‘𝑑) · 𝑑))) = ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))))
158	153, 157	eqtrd 2772	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (2↑-(!‘(𝑑 + 1))) = ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))))
159	43	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → 𝐴 ∈ ℂ)
160	110, 146, 159	addsubd 11594	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → ((𝑑 + 1) − 𝐴) = ((𝑑 − 𝐴) + 1))
161	160	oveq2d 7427	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → ((1 / 2)↑((𝑑 + 1) − 𝐴)) = ((1 / 2)↑((𝑑 − 𝐴) + 1)))
162		uznn0sub 12863	. . . . . . . . . . . . . 14 ⊢ (𝑑 ∈ (ℤ≥‘𝐴) → (𝑑 − 𝐴) ∈ ℕ0)
163	162	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (𝑑 − 𝐴) ∈ ℕ0)
164		expp1 14036	. . . . . . . . . . . . 13 ⊢ (((1 / 2) ∈ ℂ ∧ (𝑑 − 𝐴) ∈ ℕ0) → ((1 / 2)↑((𝑑 − 𝐴) + 1)) = (((1 / 2)↑(𝑑 − 𝐴)) · (1 / 2)))
165	46, 163, 164	sylancr 587	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → ((1 / 2)↑((𝑑 − 𝐴) + 1)) = (((1 / 2)↑(𝑑 − 𝐴)) · (1 / 2)))
166	161, 165	eqtrd 2772	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → ((1 / 2)↑((𝑑 + 1) − 𝐴)) = (((1 / 2)↑(𝑑 − 𝐴)) · (1 / 2)))
167	166	oveq2d 7427	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))) = ((2↑-(!‘𝐴)) · (((1 / 2)↑(𝑑 − 𝐴)) · (1 / 2))))
168	84	rpcnd 13020	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (2↑-(!‘𝐴)) ∈ ℂ)
169	92	rpcnd 13020	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → ((1 / 2)↑(𝑑 − 𝐴)) ∈ ℂ)
170	46	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (1 / 2) ∈ ℂ)
171	168, 169, 170	mulassd 11239	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) · (1 / 2)) = ((2↑-(!‘𝐴)) · (((1 / 2)↑(𝑑 − 𝐴)) · (1 / 2))))
172	167, 171	eqtr4d 2775	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))) = (((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) · (1 / 2)))
173	158, 172	breq12d 5161	. . . . . . . 8 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → ((2↑-(!‘(𝑑 + 1))) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))) ↔ ((2↑-(!‘𝑑)) · (2↑(-(!‘𝑑) · 𝑑))) ≤ (((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) · (1 / 2))))
174	134, 173	sylibrd 258	. . . . . . 7 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → ((2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) → (2↑-(!‘(𝑑 + 1))) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴)))))
175		fveq2 6891	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → (!‘𝑎) = (!‘𝑑))
176	175	negeqd 11456	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → -(!‘𝑎) = -(!‘𝑑))
177	176	oveq2d 7427	. . . . . . . . . 10 ⊢ (𝑎 = 𝑑 → (2↑-(!‘𝑎)) = (2↑-(!‘𝑑)))
178		ovex 7444	. . . . . . . . . 10 ⊢ (2↑-(!‘𝑑)) ∈ V
179	177, 5, 178	fvmpt 6998	. . . . . . . . 9 ⊢ (𝑑 ∈ ℕ → (𝐹‘𝑑) = (2↑-(!‘𝑑)))
180	70, 179	syl 17	. . . . . . . 8 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (𝐹‘𝑑) = (2↑-(!‘𝑑)))
181		oveq1 7418	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑑 → (𝑐 − 𝐴) = (𝑑 − 𝐴))
182	181	oveq2d 7427	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑑 → ((1 / 2)↑(𝑐 − 𝐴)) = ((1 / 2)↑(𝑑 − 𝐴)))
183	182	oveq2d 7427	. . . . . . . . . 10 ⊢ (𝑐 = 𝑑 → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴))) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))))
184		ovex 7444	. . . . . . . . . 10 ⊢ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) ∈ V
185	183, 65, 184	fvmpt 6998	. . . . . . . . 9 ⊢ (𝑑 ∈ (ℤ≥‘𝐴) → (𝐺‘𝑑) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))))
186	185	adantl 482	. . . . . . . 8 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (𝐺‘𝑑) = ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))))
187	180, 186	breq12d 5161	. . . . . . 7 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → ((𝐹‘𝑑) ≤ (𝐺‘𝑑) ↔ (2↑-(!‘𝑑)) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴)))))
188	70	peano2nnd 12231	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (𝑑 + 1) ∈ ℕ)
189		fveq2 6891	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝑑 + 1) → (!‘𝑎) = (!‘(𝑑 + 1)))
190	189	negeqd 11456	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑑 + 1) → -(!‘𝑎) = -(!‘(𝑑 + 1)))
191	190	oveq2d 7427	. . . . . . . . . 10 ⊢ (𝑎 = (𝑑 + 1) → (2↑-(!‘𝑎)) = (2↑-(!‘(𝑑 + 1))))
192		ovex 7444	. . . . . . . . . 10 ⊢ (2↑-(!‘(𝑑 + 1))) ∈ V
193	191, 5, 192	fvmpt 6998	. . . . . . . . 9 ⊢ ((𝑑 + 1) ∈ ℕ → (𝐹‘(𝑑 + 1)) = (2↑-(!‘(𝑑 + 1))))
194	188, 193	syl 17	. . . . . . . 8 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (𝐹‘(𝑑 + 1)) = (2↑-(!‘(𝑑 + 1))))
195		peano2uz 12887	. . . . . . . . . 10 ⊢ (𝑑 ∈ (ℤ≥‘𝐴) → (𝑑 + 1) ∈ (ℤ≥‘𝐴))
196		oveq1 7418	. . . . . . . . . . . . 13 ⊢ (𝑐 = (𝑑 + 1) → (𝑐 − 𝐴) = ((𝑑 + 1) − 𝐴))
197	196	oveq2d 7427	. . . . . . . . . . . 12 ⊢ (𝑐 = (𝑑 + 1) → ((1 / 2)↑(𝑐 − 𝐴)) = ((1 / 2)↑((𝑑 + 1) − 𝐴)))
198	197	oveq2d 7427	. . . . . . . . . . 11 ⊢ (𝑐 = (𝑑 + 1) → ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴))) = ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))))
199		ovex 7444	. . . . . . . . . . 11 ⊢ ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))) ∈ V
200	198, 65, 199	fvmpt 6998	. . . . . . . . . 10 ⊢ ((𝑑 + 1) ∈ (ℤ≥‘𝐴) → (𝐺‘(𝑑 + 1)) = ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))))
201	195, 200	syl 17	. . . . . . . . 9 ⊢ (𝑑 ∈ (ℤ≥‘𝐴) → (𝐺‘(𝑑 + 1)) = ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))))
202	201	adantl 482	. . . . . . . 8 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → (𝐺‘(𝑑 + 1)) = ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))))
203	194, 202	breq12d 5161	. . . . . . 7 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → ((𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1)) ↔ (2↑-(!‘(𝑑 + 1))) ≤ ((2↑-(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴)))))
204	174, 187, 203	3imtr4d 293	. . . . . 6 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ≥‘𝐴)) → ((𝐹‘𝑑) ≤ (𝐺‘𝑑) → (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1))))
205	204	expcom 414	. . . . 5 ⊢ (𝑑 ∈ (ℤ≥‘𝐴) → (𝐴 ∈ ℕ → ((𝐹‘𝑑) ≤ (𝐺‘𝑑) → (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1)))))
206	205	a2d 29	. . . 4 ⊢ (𝑑 ∈ (ℤ≥‘𝐴) → ((𝐴 ∈ ℕ → (𝐹‘𝑑) ≤ (𝐺‘𝑑)) → (𝐴 ∈ ℕ → (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1)))))
207	22, 26, 30, 34, 69, 206	uzind4i 12896	. . 3 ⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (𝐴 ∈ ℕ → (𝐹‘𝐵) ≤ (𝐺‘𝐵)))
208	207	impcom 408	. 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐹‘𝐵) ≤ (𝐺‘𝐵))
209		0xr 11263	. . 3 ⊢ 0 ∈ ℝ*
210	65	aaliou3lem1 25862	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐺‘𝐵) ∈ ℝ)
211		elioc2 13389	. . 3 ⊢ ((0 ∈ ℝ* ∧ (𝐺‘𝐵) ∈ ℝ) → ((𝐹‘𝐵) ∈ (0(,](𝐺‘𝐵)) ↔ ((𝐹‘𝐵) ∈ ℝ ∧ 0 < (𝐹‘𝐵) ∧ (𝐹‘𝐵) ≤ (𝐺‘𝐵))))
212	209, 210, 211	sylancr 587	. 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → ((𝐹‘𝐵) ∈ (0(,](𝐺‘𝐵)) ↔ ((𝐹‘𝐵) ∈ ℝ ∧ 0 < (𝐹‘𝐵) ∧ (𝐹‘𝐵) ≤ (𝐺‘𝐵))))
213	17, 18, 208, 212	mpbir3and 1342	1 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐹‘𝐵) ∈ (0(,](𝐺‘𝐵)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2940   class class class wbr 5148   ↦ cmpt 5231  ‘cfv 6543  (class class class)co 7411  ℂcc 11110  ℝcr 11111  0cc0 11112  1c1 11113   + caddc 11115   · cmul 11117  ℝ^*cxr 11249   < clt 11250   ≤ cle 11251   − cmin 11446  -cneg 11447   / cdiv 11873  ℕcn 12214  2c2 12269  ℕ₀cn0 12474  ℤcz 12560  ℤ_≥cuz 12824  ℝ⁺crp 12976  (,]cioc 13327  ↑cexp 14029  !cfa 14235

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-n0 12475  df-z 12561  df-uz 12825  df-rp 12977  df-ioc 13331  df-seq 13969  df-exp 14030  df-fac 14236

This theorem is referenced by:  aaliou3lem3  25864