aaliou3lem2 - Metamath Proof Explorer

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

Theorem aaliou3lem2 26727

Description: Lemma for aaliou3 26735. (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 13085	. . . . 5 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ_≥‘𝐴)) → 𝐵 ∈ ℕ)
2		fveq2 6916	. . . . . . . 8 ⊢ (𝑎 = 𝐵 → (!‘𝑎) = (!‘𝐵))
3	2	negeqd 11590	. . . . . . 7 ⊢ (𝑎 = 𝐵 → -(!‘𝑎) = -(!‘𝐵))
4	3	oveq2d 7467	. . . . . 6 ⊢ (𝑎 = 𝐵 → (2↑ -(!‘𝑎)) = (2↑ -(!‘𝐵)))
5		aaliou3lem.b	. . . . . 6 ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑ -(!‘𝑎)))
6		ovex 7484	. . . . . 6 ⊢ (2↑ -(!‘𝐵)) ∈ V
7	4, 5, 6	fvmpt 7024	. . . . 5 ⊢ (𝐵 ∈ ℕ → (𝐹‘𝐵) = (2↑ -(!‘𝐵)))
8	1, 7	syl 18	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ_≥‘𝐴)) → (𝐹‘𝐵) = (2↑ -(!‘𝐵)))
9		2rp 13165	. . . . 5 ⊢ 2 ∈ ℝ⁺
10	1	nnnn0d 12707	. . . . . . . 8 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ_≥‘𝐴)) → 𝐵 ∈ ℕ₀)
11	10	faccld 14469	. . . . . . 7 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ_≥‘𝐴)) → (!‘𝐵) ∈ ℕ)
12	11	nnzd 12759	. . . . . 6 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ_≥‘𝐴)) → (!‘𝐵) ∈ ℤ)
13	12	znegcld 12845	. . . . 5 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ_≥‘𝐴)) → -(!‘𝐵) ∈ ℤ)
14		rpexpcl 14263	. . . . 5 ⊢ ((2 ∈ ℝ⁺ ∧ -(!‘𝐵) ∈ ℤ) → (2↑ -(!‘𝐵)) ∈ ℝ⁺)
15	9, 13, 14	sylancr 599	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ_≥‘𝐴)) → (2↑ -(!‘𝐵)) ∈ ℝ⁺)
16	8, 15	eqeltrd 2864	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ_≥‘𝐴)) → (𝐹‘𝐵) ∈ ℝ⁺)
17	16	rpred 13204	. 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ_≥‘𝐴)) → (𝐹‘𝐵) ∈ ℝ)
18	16	rpgt0d 13207	. 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ_≥‘𝐴)) → 0 < (𝐹‘𝐵))
19		fveq2 6916	. . . . . 6 ⊢ (𝑏 = 𝐴 → (𝐹‘𝑏) = (𝐹‘𝐴))
20		fveq2 6916	. . . . . 6 ⊢ (𝑏 = 𝐴 → (𝐺‘𝑏) = (𝐺‘𝐴))
21	19, 20	breq12d 5121	. . . . 5 ⊢ (𝑏 = 𝐴 → ((𝐹‘𝑏) ≤ (𝐺‘𝑏) ↔ (𝐹‘𝐴) ≤ (𝐺‘𝐴)))
22	21	imbi2d 343	. . . 4 ⊢ (𝑏 = 𝐴 → ((𝐴 ∈ ℕ → (𝐹‘𝑏) ≤ (𝐺‘𝑏)) ↔ (𝐴 ∈ ℕ → (𝐹‘𝐴) ≤ (𝐺‘𝐴))))
23		fveq2 6916	. . . . . 6 ⊢ (𝑏 = 𝑑 → (𝐹‘𝑏) = (𝐹‘𝑑))
24		fveq2 6916	. . . . . 6 ⊢ (𝑏 = 𝑑 → (𝐺‘𝑏) = (𝐺‘𝑑))
25	23, 24	breq12d 5121	. . . . 5 ⊢ (𝑏 = 𝑑 → ((𝐹‘𝑏) ≤ (𝐺‘𝑏) ↔ (𝐹‘𝑑) ≤ (𝐺‘𝑑)))
26	25	imbi2d 343	. . . 4 ⊢ (𝑏 = 𝑑 → ((𝐴 ∈ ℕ → (𝐹‘𝑏) ≤ (𝐺‘𝑏)) ↔ (𝐴 ∈ ℕ → (𝐹‘𝑑) ≤ (𝐺‘𝑑))))
27		fveq2 6916	. . . . . 6 ⊢ (𝑏 = (𝑑 + 1) → (𝐹‘𝑏) = (𝐹‘(𝑑 + 1)))
28		fveq2 6916	. . . . . 6 ⊢ (𝑏 = (𝑑 + 1) → (𝐺‘𝑏) = (𝐺‘(𝑑 + 1)))
29	27, 28	breq12d 5121	. . . . 5 ⊢ (𝑏 = (𝑑 + 1) → ((𝐹‘𝑏) ≤ (𝐺‘𝑏) ↔ (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1))))
30	29	imbi2d 343	. . . 4 ⊢ (𝑏 = (𝑑 + 1) → ((𝐴 ∈ ℕ → (𝐹‘𝑏) ≤ (𝐺‘𝑏)) ↔ (𝐴 ∈ ℕ → (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1)))))
31		fveq2 6916	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝐹‘𝑏) = (𝐹‘𝐵))
32		fveq2 6916	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝐺‘𝑏) = (𝐺‘𝐵))
33	31, 32	breq12d 5121	. . . . 5 ⊢ (𝑏 = 𝐵 → ((𝐹‘𝑏) ≤ (𝐺‘𝑏) ↔ (𝐹‘𝐵) ≤ (𝐺‘𝐵)))
34	33	imbi2d 343	. . . 4 ⊢ (𝑏 = 𝐵 → ((𝐴 ∈ ℕ → (𝐹‘𝑏) ≤ (𝐺‘𝑏)) ↔ (𝐴 ∈ ℕ → (𝐹‘𝐵) ≤ (𝐺‘𝐵))))
35		nnnn0 12653	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ₀)
36	35	faccld 14469	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℕ → (!‘𝐴) ∈ ℕ)
37	36	nnzd 12759	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℕ → (!‘𝐴) ∈ ℤ)
38	37	znegcld 12845	. . . . . . . . 9 ⊢ (𝐴 ∈ ℕ → -(!‘𝐴) ∈ ℤ)
39		rpexpcl 14263	. . . . . . . . 9 ⊢ ((2 ∈ ℝ⁺ ∧ -(!‘𝐴) ∈ ℤ) → (2↑ -(!‘𝐴)) ∈ ℝ⁺)
40	9, 38, 39	sylancr 599	. . . . . . . 8 ⊢ (𝐴 ∈ ℕ → (2↑ -(!‘𝐴)) ∈ ℝ⁺)
41	40	rpred 13204	. . . . . . 7 ⊢ (𝐴 ∈ ℕ → (2↑ -(!‘𝐴)) ∈ ℝ)
42	41	leidd 11922	. . . . . 6 ⊢ (𝐴 ∈ ℕ → (2↑ -(!‘𝐴)) ≤ (2↑ -(!‘𝐴)))
43		nncn 12383	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
44	43	subidd 11696	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℕ → (𝐴 − 𝐴) = 0)
45	44	oveq2d 7467	. . . . . . . . 9 ⊢ (𝐴 ∈ ℕ → ((1 / 2)↑(𝐴 − 𝐴)) = ((1 / 2)↑0))
46		halfcn 12600	. . . . . . . . . 10 ⊢ (1 / 2) ∈ ℂ
47		exp0 14248	. . . . . . . . . 10 ⊢ ((1 / 2) ∈ ℂ → ((1 / 2)↑0) = 1)
48	46, 47	ax-mp 5	. . . . . . . . 9 ⊢ ((1 / 2)↑0) = 1
49	45, 48	eqtrdi 2814	. . . . . . . 8 ⊢ (𝐴 ∈ ℕ → ((1 / 2)↑(𝐴 − 𝐴)) = 1)
50	49	oveq2d 7467	. . . . . . 7 ⊢ (𝐴 ∈ ℕ → ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝐴 − 𝐴))) = ((2↑ -(!‘𝐴)) · 1))
51	40	rpcnd 13206	. . . . . . . 8 ⊢ (𝐴 ∈ ℕ → (2↑ -(!‘𝐴)) ∈ ℂ)
52	51	mulridd 11365	. . . . . . 7 ⊢ (𝐴 ∈ ℕ → ((2↑ -(!‘𝐴)) · 1) = (2↑ -(!‘𝐴)))
53	50, 52	eqtrd 2798	. . . . . 6 ⊢ (𝐴 ∈ ℕ → ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝐴 − 𝐴))) = (2↑ -(!‘𝐴)))
54	42, 53	breqtrrd 5139	. . . . 5 ⊢ (𝐴 ∈ ℕ → (2↑ -(!‘𝐴)) ≤ ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝐴 − 𝐴))))
55		fveq2 6916	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → (!‘𝑎) = (!‘𝐴))
56	55	negeqd 11590	. . . . . . 7 ⊢ (𝑎 = 𝐴 → -(!‘𝑎) = -(!‘𝐴))
57	56	oveq2d 7467	. . . . . 6 ⊢ (𝑎 = 𝐴 → (2↑ -(!‘𝑎)) = (2↑ -(!‘𝐴)))
58		ovex 7484	. . . . . 6 ⊢ (2↑ -(!‘𝐴)) ∈ V
59	57, 5, 58	fvmpt 7024	. . . . 5 ⊢ (𝐴 ∈ ℕ → (𝐹‘𝐴) = (2↑ -(!‘𝐴)))
60		nnz 12754	. . . . . 6 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℤ)
61		uzid 13020	. . . . . 6 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ (ℤ_≥‘𝐴))
62		oveq1 7458	. . . . . . . . 9 ⊢ (𝑐 = 𝐴 → (𝑐 − 𝐴) = (𝐴 − 𝐴))
63	62	oveq2d 7467	. . . . . . . 8 ⊢ (𝑐 = 𝐴 → ((1 / 2)↑(𝑐 − 𝐴)) = ((1 / 2)↑(𝐴 − 𝐴)))
64	63	oveq2d 7467	. . . . . . 7 ⊢ (𝑐 = 𝐴 → ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴))) = ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝐴 − 𝐴))))
65		aaliou3lem.a	. . . . . . 7 ⊢ 𝐺 = (𝑐 ∈ (ℤ_≥‘𝐴) ↦ ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴))))
66		ovex 7484	. . . . . . 7 ⊢ ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝐴 − 𝐴))) ∈ V
67	64, 65, 66	fvmpt 7024	. . . . . 6 ⊢ (𝐴 ∈ (ℤ_≥‘𝐴) → (𝐺‘𝐴) = ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝐴 − 𝐴))))
68	60, 61, 67	3syl 19	. . . . 5 ⊢ (𝐴 ∈ ℕ → (𝐺‘𝐴) = ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝐴 − 𝐴))))
69	54, 59, 68	3brtr4d 5143	. . . 4 ⊢ (𝐴 ∈ ℕ → (𝐹‘𝐴) ≤ (𝐺‘𝐴))
70		eluznn 13085	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → 𝑑 ∈ ℕ)
71	70	nnnn0d 12707	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → 𝑑 ∈ ℕ₀)
72	71	faccld 14469	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (!‘𝑑) ∈ ℕ)
73	72	nnzd 12759	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (!‘𝑑) ∈ ℤ)
74	73	znegcld 12845	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → -(!‘𝑑) ∈ ℤ)
75		rpexpcl 14263	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ⁺ ∧ -(!‘𝑑) ∈ ℤ) → (2↑ -(!‘𝑑)) ∈ ℝ⁺)
76	9, 74, 75	sylancr 599	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (2↑ -(!‘𝑑)) ∈ ℝ⁺)
77	76	rpred 13204	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (2↑ -(!‘𝑑)) ∈ ℝ)
78	76	rpge0d 13208	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → 0 ≤ (2↑ -(!‘𝑑)))
79		simpl 488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → 𝐴 ∈ ℕ)
80	79	nnnn0d 12707	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → 𝐴 ∈ ℕ₀)
81	80	faccld 14469	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (!‘𝐴) ∈ ℕ)
82	81	nnzd 12759	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (!‘𝐴) ∈ ℤ)
83	82	znegcld 12845	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → -(!‘𝐴) ∈ ℤ)
84	9, 83, 39	sylancr 599	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (2↑ -(!‘𝐴)) ∈ ℝ⁺)
85		halfre 12599	. . . . . . . . . . . . . . . 16 ⊢ (1 / 2) ∈ ℝ
86		halfgt0 12601	. . . . . . . . . . . . . . . 16 ⊢ 0 < (1 / 2)
87	85, 86	elrpii 13163	. . . . . . . . . . . . . . 15 ⊢ (1 / 2) ∈ ℝ⁺
88		eluzelz 13015	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ (ℤ_≥‘𝐴) → 𝑑 ∈ ℤ)
89		zsubcl 12778	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑑 − 𝐴) ∈ ℤ)
90	88, 60, 89	syl2anr 609	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (𝑑 − 𝐴) ∈ ℤ)
91		rpexpcl 14263	. . . . . . . . . . . . . . 15 ⊢ (((1 / 2) ∈ ℝ⁺ ∧ (𝑑 − 𝐴) ∈ ℤ) → ((1 / 2)↑(𝑑 − 𝐴)) ∈ ℝ⁺)
92	87, 90, 91	sylancr 599	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ((1 / 2)↑(𝑑 − 𝐴)) ∈ ℝ⁺)
93	84, 92	rpmulcld 13220	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) ∈ ℝ⁺)
94	93	rpred 13204	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) ∈ ℝ)
95	77, 78, 94	jca31 524	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (((2↑ -(!‘𝑑)) ∈ ℝ ∧ 0 ≤ (2↑ -(!‘𝑑))) ∧ ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) ∈ ℝ))
96	95	adantr 486	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) ∧ (2↑ -(!‘𝑑)) ≤ ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴)))) → (((2↑ -(!‘𝑑)) ∈ ℝ ∧ 0 ≤ (2↑ -(!‘𝑑))) ∧ ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) ∈ ℝ))
97	88	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → 𝑑 ∈ ℤ)
98	74, 97	zmulcld 12849	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ( -(!‘𝑑) · 𝑑) ∈ ℤ)
99		rpexpcl 14263	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ⁺ ∧ ( -(!‘𝑑) · 𝑑) ∈ ℤ) → (2↑( -(!‘𝑑) · 𝑑)) ∈ ℝ⁺)
100	9, 98, 99	sylancr 599	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (2↑( -(!‘𝑑) · 𝑑)) ∈ ℝ⁺)
101	100	rpred 13204	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (2↑( -(!‘𝑑) · 𝑑)) ∈ ℝ)
102	100	rpge0d 13208	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → 0 ≤ (2↑( -(!‘𝑑) · 𝑑)))
103	85	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (1 / 2) ∈ ℝ)
104	101, 102, 103	jca31 524	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (((2↑( -(!‘𝑑) · 𝑑)) ∈ ℝ ∧ 0 ≤ (2↑( -(!‘𝑑) · 𝑑))) ∧ (1 / 2) ∈ ℝ))
105	104	adantr 486	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) ∧ (2↑ -(!‘𝑑)) ≤ ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴)))) → (((2↑( -(!‘𝑑) · 𝑑)) ∈ ℝ ∧ 0 ≤ (2↑( -(!‘𝑑) · 𝑑))) ∧ (1 / 2) ∈ ℝ))
106		simpr 490	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) ∧ (2↑ -(!‘𝑑)) ≤ ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴)))) → (2↑ -(!‘𝑑)) ≤ ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))))
107		2re 12457	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
108		1le2 12594	. . . . . . . . . . . . 13 ⊢ 1 ≤ 2
109	72	nncnd 12391	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (!‘𝑑) ∈ ℂ)
110	97	zcnd 12844	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → 𝑑 ∈ ℂ)
111	109, 110	mulneg1d 11808	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ( -(!‘𝑑) · 𝑑) = -((!‘𝑑) · 𝑑))
112	72, 70	nnmulcld 12431	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ((!‘𝑑) · 𝑑) ∈ ℕ)
113	112	nnge1d 12426	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → 1 ≤ ((!‘𝑑) · 𝑑))
114		1re 11347	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
115	112	nnred 12390	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ((!‘𝑑) · 𝑑) ∈ ℝ)
116		leneg 11859	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℝ ∧ ((!‘𝑑) · 𝑑) ∈ ℝ) → (1 ≤ ((!‘𝑑) · 𝑑) ↔ -((!‘𝑑) · 𝑑) ≤ -1))
117	114, 115, 116	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (1 ≤ ((!‘𝑑) · 𝑑) ↔ -((!‘𝑑) · 𝑑) ≤ -1))
118	113, 117	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → -((!‘𝑑) · 𝑑) ≤ -1)
119	111, 118	eqbrtrd 5133	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ( -(!‘𝑑) · 𝑑) ≤ -1)
120		neg1z 12772	. . . . . . . . . . . . . . 15 ⊢ -1 ∈ ℤ
121		eluz 13019	. . . . . . . . . . . . . . 15 ⊢ ((( -(!‘𝑑) · 𝑑) ∈ ℤ ∧ -1 ∈ ℤ) → ( -1 ∈ (ℤ_≥‘( -(!‘𝑑) · 𝑑)) ↔ ( -(!‘𝑑) · 𝑑) ≤ -1))
122	98, 120, 121	sylancl 598	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ( -1 ∈ (ℤ_≥‘( -(!‘𝑑) · 𝑑)) ↔ ( -(!‘𝑑) · 𝑑) ≤ -1))
123	119, 122	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → -1 ∈ (ℤ_≥‘( -(!‘𝑑) · 𝑑)))
124		leexp2a 14355	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ ∧ 1 ≤ 2 ∧ -1 ∈ (ℤ_≥‘( -(!‘𝑑) · 𝑑))) → (2↑( -(!‘𝑑) · 𝑑)) ≤ (2↑ -1))
125	107, 108, 123, 124	mp3an12i 1495	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (2↑( -(!‘𝑑) · 𝑑)) ≤ (2↑ -1))
126		2cn 12458	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℂ
127		expn1 14254	. . . . . . . . . . . . 13 ⊢ (2 ∈ ℂ → (2↑ -1) = (1 / 2))
128	126, 127	ax-mp 5	. . . . . . . . . . . 12 ⊢ (2↑ -1) = (1 / 2)
129	125, 128	breqtrdi 5152	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (2↑( -(!‘𝑑) · 𝑑)) ≤ (1 / 2))
130	129	adantr 486	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) ∧ (2↑ -(!‘𝑑)) ≤ ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴)))) → (2↑( -(!‘𝑑) · 𝑑)) ≤ (1 / 2))
131		lemul12a 12215	. . . . . . . . . . 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 1135	. . . . . . . . . 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 1402	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) ∧ (2↑ -(!‘𝑑)) ≤ ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴)))) → ((2↑ -(!‘𝑑)) · (2↑( -(!‘𝑑) · 𝑑))) ≤ (((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) · (1 / 2)))
134	133	ex 418	. . . . . . . 8 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ((2↑ -(!‘𝑑)) ≤ ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) → ((2↑ -(!‘𝑑)) · (2↑( -(!‘𝑑) · 𝑑))) ≤ (((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) · (1 / 2))))
135		facp1 14463	. . . . . . . . . . . . . 14 ⊢ (𝑑 ∈ ℕ₀ → (!‘(𝑑 + 1)) = ((!‘𝑑) · (𝑑 + 1)))
136	71, 135	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (!‘(𝑑 + 1)) = ((!‘𝑑) · (𝑑 + 1)))
137	136	negeqd 11590	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → -(!‘(𝑑 + 1)) = -((!‘𝑑) · (𝑑 + 1)))
138		ax-1cn 11297	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
139		addcom 11535	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑑 + 1) = (1 + 𝑑))
140	110, 138, 139	sylancl 598	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (𝑑 + 1) = (1 + 𝑑))
141	140	oveq2d 7467	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ( -(!‘𝑑) · (𝑑 + 1)) = ( -(!‘𝑑) · (1 + 𝑑)))
142		peano2cn 11521	. . . . . . . . . . . . . . 15 ⊢ (𝑑 ∈ ℂ → (𝑑 + 1) ∈ ℂ)
143	110, 142	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (𝑑 + 1) ∈ ℂ)
144	109, 143	mulneg1d 11808	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ( -(!‘𝑑) · (𝑑 + 1)) = -((!‘𝑑) · (𝑑 + 1)))
145	74	zcnd 12844	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → -(!‘𝑑) ∈ ℂ)
146		1cnd 11341	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → 1 ∈ ℂ)
147	145, 146, 110	adddid 11372	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ( -(!‘𝑑) · (1 + 𝑑)) = (( -(!‘𝑑) · 1) + ( -(!‘𝑑) · 𝑑)))
148	145	mulridd 11365	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ( -(!‘𝑑) · 1) = -(!‘𝑑))
149	148	oveq1d 7466	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (( -(!‘𝑑) · 1) + ( -(!‘𝑑) · 𝑑)) = ( -(!‘𝑑) + ( -(!‘𝑑) · 𝑑)))
150	147, 149	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ( -(!‘𝑑) · (1 + 𝑑)) = ( -(!‘𝑑) + ( -(!‘𝑑) · 𝑑)))
151	141, 144, 150	3eqtr3d 2806	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → -((!‘𝑑) · (𝑑 + 1)) = ( -(!‘𝑑) + ( -(!‘𝑑) · 𝑑)))
152	137, 151	eqtrd 2798	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → -(!‘(𝑑 + 1)) = ( -(!‘𝑑) + ( -(!‘𝑑) · 𝑑)))
153	152	oveq2d 7467	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (2↑ -(!‘(𝑑 + 1))) = (2↑( -(!‘𝑑) + ( -(!‘𝑑) · 𝑑))))
154		2cnne0 12595	. . . . . . . . . . . 12 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
155		expaddz 14289	. . . . . . . . . . . 12 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ ( -(!‘𝑑) ∈ ℤ ∧ ( -(!‘𝑑) · 𝑑) ∈ ℤ)) → (2↑( -(!‘𝑑) + ( -(!‘𝑑) · 𝑑))) = ((2↑ -(!‘𝑑)) · (2↑( -(!‘𝑑) · 𝑑))))
156	154, 155	mpan 703	. . . . . . . . . . 11 ⊢ (( -(!‘𝑑) ∈ ℤ ∧ ( -(!‘𝑑) · 𝑑) ∈ ℤ) → (2↑( -(!‘𝑑) + ( -(!‘𝑑) · 𝑑))) = ((2↑ -(!‘𝑑)) · (2↑( -(!‘𝑑) · 𝑑))))
157	74, 98, 156	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (2↑( -(!‘𝑑) + ( -(!‘𝑑) · 𝑑))) = ((2↑ -(!‘𝑑)) · (2↑( -(!‘𝑑) · 𝑑))))
158	153, 157	eqtrd 2798	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (2↑ -(!‘(𝑑 + 1))) = ((2↑ -(!‘𝑑)) · (2↑( -(!‘𝑑) · 𝑑))))
159	43	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → 𝐴 ∈ ℂ)
160	110, 146, 159	addsubd 11729	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ((𝑑 + 1) − 𝐴) = ((𝑑 − 𝐴) + 1))
161	160	oveq2d 7467	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ((1 / 2)↑((𝑑 + 1) − 𝐴)) = ((1 / 2)↑((𝑑 − 𝐴) + 1)))
162		uznn0sub 13040	. . . . . . . . . . . . . 14 ⊢ (𝑑 ∈ (ℤ_≥‘𝐴) → (𝑑 − 𝐴) ∈ ℕ₀)
163	162	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (𝑑 − 𝐴) ∈ ℕ₀)
164		expp1 14251	. . . . . . . . . . . . 13 ⊢ (((1 / 2) ∈ ℂ ∧ (𝑑 − 𝐴) ∈ ℕ₀) → ((1 / 2)↑((𝑑 − 𝐴) + 1)) = (((1 / 2)↑(𝑑 − 𝐴)) · (1 / 2)))
165	46, 163, 164	sylancr 599	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ((1 / 2)↑((𝑑 − 𝐴) + 1)) = (((1 / 2)↑(𝑑 − 𝐴)) · (1 / 2)))
166	161, 165	eqtrd 2798	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ((1 / 2)↑((𝑑 + 1) − 𝐴)) = (((1 / 2)↑(𝑑 − 𝐴)) · (1 / 2)))
167	166	oveq2d 7467	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ((2↑ -(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))) = ((2↑ -(!‘𝐴)) · (((1 / 2)↑(𝑑 − 𝐴)) · (1 / 2))))
168	84	rpcnd 13206	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (2↑ -(!‘𝐴)) ∈ ℂ)
169	92	rpcnd 13206	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ((1 / 2)↑(𝑑 − 𝐴)) ∈ ℂ)
170	46	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (1 / 2) ∈ ℂ)
171	168, 169, 170	mulassd 11371	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) · (1 / 2)) = ((2↑ -(!‘𝐴)) · (((1 / 2)↑(𝑑 − 𝐴)) · (1 / 2))))
172	167, 171	eqtr4d 2801	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ((2↑ -(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))) = (((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) · (1 / 2)))
173	158, 172	breq12d 5121	. . . . . . . 8 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ((2↑ -(!‘(𝑑 + 1))) ≤ ((2↑ -(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))) ↔ ((2↑ -(!‘𝑑)) · (2↑( -(!‘𝑑) · 𝑑))) ≤ (((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) · (1 / 2))))
174	134, 173	sylibrd 262	. . . . . . 7 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ((2↑ -(!‘𝑑)) ≤ ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) → (2↑ -(!‘(𝑑 + 1))) ≤ ((2↑ -(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴)))))
175		fveq2 6916	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → (!‘𝑎) = (!‘𝑑))
176	175	negeqd 11590	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → -(!‘𝑎) = -(!‘𝑑))
177	176	oveq2d 7467	. . . . . . . . . 10 ⊢ (𝑎 = 𝑑 → (2↑ -(!‘𝑎)) = (2↑ -(!‘𝑑)))
178		ovex 7484	. . . . . . . . . 10 ⊢ (2↑ -(!‘𝑑)) ∈ V
179	177, 5, 178	fvmpt 7024	. . . . . . . . 9 ⊢ (𝑑 ∈ ℕ → (𝐹‘𝑑) = (2↑ -(!‘𝑑)))
180	70, 179	syl 18	. . . . . . . 8 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (𝐹‘𝑑) = (2↑ -(!‘𝑑)))
181		oveq1 7458	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑑 → (𝑐 − 𝐴) = (𝑑 − 𝐴))
182	181	oveq2d 7467	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑑 → ((1 / 2)↑(𝑐 − 𝐴)) = ((1 / 2)↑(𝑑 − 𝐴)))
183	182	oveq2d 7467	. . . . . . . . . 10 ⊢ (𝑐 = 𝑑 → ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴))) = ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))))
184		ovex 7484	. . . . . . . . . 10 ⊢ ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))) ∈ V
185	183, 65, 184	fvmpt 7024	. . . . . . . . 9 ⊢ (𝑑 ∈ (ℤ_≥‘𝐴) → (𝐺‘𝑑) = ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))))
186	185	adantl 487	. . . . . . . 8 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (𝐺‘𝑑) = ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴))))
187	180, 186	breq12d 5121	. . . . . . 7 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ((𝐹‘𝑑) ≤ (𝐺‘𝑑) ↔ (2↑ -(!‘𝑑)) ≤ ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑑 − 𝐴)))))
188	70	peano2nnd 12392	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (𝑑 + 1) ∈ ℕ)
189		fveq2 6916	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝑑 + 1) → (!‘𝑎) = (!‘(𝑑 + 1)))
190	189	negeqd 11590	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑑 + 1) → -(!‘𝑎) = -(!‘(𝑑 + 1)))
191	190	oveq2d 7467	. . . . . . . . . 10 ⊢ (𝑎 = (𝑑 + 1) → (2↑ -(!‘𝑎)) = (2↑ -(!‘(𝑑 + 1))))
192		ovex 7484	. . . . . . . . . 10 ⊢ (2↑ -(!‘(𝑑 + 1))) ∈ V
193	191, 5, 192	fvmpt 7024	. . . . . . . . 9 ⊢ ((𝑑 + 1) ∈ ℕ → (𝐹‘(𝑑 + 1)) = (2↑ -(!‘(𝑑 + 1))))
194	188, 193	syl 18	. . . . . . . 8 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (𝐹‘(𝑑 + 1)) = (2↑ -(!‘(𝑑 + 1))))
195		peano2uz 13068	. . . . . . . . . 10 ⊢ (𝑑 ∈ (ℤ_≥‘𝐴) → (𝑑 + 1) ∈ (ℤ_≥‘𝐴))
196		oveq1 7458	. . . . . . . . . . . . 13 ⊢ (𝑐 = (𝑑 + 1) → (𝑐 − 𝐴) = ((𝑑 + 1) − 𝐴))
197	196	oveq2d 7467	. . . . . . . . . . . 12 ⊢ (𝑐 = (𝑑 + 1) → ((1 / 2)↑(𝑐 − 𝐴)) = ((1 / 2)↑((𝑑 + 1) − 𝐴)))
198	197	oveq2d 7467	. . . . . . . . . . 11 ⊢ (𝑐 = (𝑑 + 1) → ((2↑ -(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴))) = ((2↑ -(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))))
199		ovex 7484	. . . . . . . . . . 11 ⊢ ((2↑ -(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))) ∈ V
200	198, 65, 199	fvmpt 7024	. . . . . . . . . 10 ⊢ ((𝑑 + 1) ∈ (ℤ_≥‘𝐴) → (𝐺‘(𝑑 + 1)) = ((2↑ -(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))))
201	195, 200	syl 18	. . . . . . . . 9 ⊢ (𝑑 ∈ (ℤ_≥‘𝐴) → (𝐺‘(𝑑 + 1)) = ((2↑ -(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))))
202	201	adantl 487	. . . . . . . 8 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → (𝐺‘(𝑑 + 1)) = ((2↑ -(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴))))
203	194, 202	breq12d 5121	. . . . . . 7 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ((𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1)) ↔ (2↑ -(!‘(𝑑 + 1))) ≤ ((2↑ -(!‘𝐴)) · ((1 / 2)↑((𝑑 + 1) − 𝐴)))))
204	174, 187, 203	3imtr4d 297	. . . . . 6 ⊢ ((𝐴 ∈ ℕ ∧ 𝑑 ∈ (ℤ_≥‘𝐴)) → ((𝐹‘𝑑) ≤ (𝐺‘𝑑) → (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1))))
205	204	expcom 419	. . . . 5 ⊢ (𝑑 ∈ (ℤ_≥‘𝐴) → (𝐴 ∈ ℕ → ((𝐹‘𝑑) ≤ (𝐺‘𝑑) → (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1)))))
206	205	a2d 30	. . . 4 ⊢ (𝑑 ∈ (ℤ_≥‘𝐴) → ((𝐴 ∈ ℕ → (𝐹‘𝑑) ≤ (𝐺‘𝑑)) → (𝐴 ∈ ℕ → (𝐹‘(𝑑 + 1)) ≤ (𝐺‘(𝑑 + 1)))))
207	22, 26, 30, 34, 69, 206	uzind4i 13077	. . 3 ⊢ (𝐵 ∈ (ℤ_≥‘𝐴) → (𝐴 ∈ ℕ → (𝐹‘𝐵) ≤ (𝐺‘𝐵)))
208	207	impcom 413	. 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ_≥‘𝐴)) → (𝐹‘𝐵) ≤ (𝐺‘𝐵))
209		0xr 11395	. . 3 ⊢ 0 ∈ ℝ^*
210	65	aaliou3lem1 26726	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ_≥‘𝐴)) → (𝐺‘𝐵) ∈ ℝ)
211		elioc2 13580	. . 3 ⊢ ((0 ∈ ℝ^* ∧ (𝐺‘𝐵) ∈ ℝ) → ((𝐹‘𝐵) ∈ (0(,](𝐺‘𝐵)) ↔ ((𝐹‘𝐵) ∈ ℝ ∧ 0 < (𝐹‘𝐵) ∧ (𝐹‘𝐵) ≤ (𝐺‘𝐵))))
212	209, 210, 211	sylancr 599	. 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ_≥‘𝐴)) → ((𝐹‘𝐵) ∈ (0(,](𝐺‘𝐵)) ↔ ((𝐹‘𝐵) ∈ ℝ ∧ 0 < (𝐹‘𝐵) ∧ (𝐹‘𝐵) ≤ (𝐺‘𝐵))))
213	17, 18, 208, 212	mpbir3and 1361	1 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ_≥‘𝐴)) → (𝐹‘𝐵) ∈ (0(,](𝐺‘𝐵)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 class class class wbr 5108 ↦ cmpt 5192 ‘cfv 6566 (class class class)co 7451 ℂcc 11237 ℝcr 11238 0cc0 11239 1c1 11240 + caddc 11242 · cmul 11244 ℝ^*cxr 11381 < clt 11382 ≤ cle 11383 − cmin 11580 -cneg 11581 / cdiv 12013 ℕcn 12375 2c2 12437 ℕ₀cn0 12646 ℤcz 12733 ℤ_≥cuz 13005 ℝ⁺crp 13160 (,]cioc 13517 ↑cexp 14244 !cfa 14458

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4841 df-uni 4873 df-iun 4958 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-om 7912 df-2nd 8036 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-er 8755 df-en 9012 df-dom 9013 df-sdom 9014 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-div 12014 df-nn 12376 df-2 12445 df-n0 12647 df-z 12734 df-uz 13006 df-rp 13161 df-ioc 13521 df-seq 14185 df-exp 14245 df-fac 14459

This theorem is used by: aaliou3lem3 26728

W3C validator