Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem7 Structured version   Visualization version   GIF version

Theorem stoweidlem7 41721
Description: This lemma is used to prove that qn as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91, (at the top of page 91), is such that qn < ε on 𝑇𝑈, and qn > 1 - ε on 𝑉. Here it is proven that, for 𝑛 large enough, 1-(k*δ/2)^n > 1 - ε , and 1/(k*δ)^n < ε. The variable 𝐴 is used to represent (k*δ) in the paper, and 𝐵 is used to represent (k*δ/2). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem7.1 𝐹 = (𝑖 ∈ ℕ0 ↦ ((1 / 𝐴)↑𝑖))
stoweidlem7.2 𝐺 = (𝑖 ∈ ℕ0 ↦ (𝐵𝑖))
stoweidlem7.3 (𝜑𝐴 ∈ ℝ)
stoweidlem7.4 (𝜑 → 1 < 𝐴)
stoweidlem7.5 (𝜑𝐵 ∈ ℝ+)
stoweidlem7.6 (𝜑𝐵 < 1)
stoweidlem7.7 (𝜑𝐸 ∈ ℝ+)
Assertion
Ref Expression
stoweidlem7 (𝜑 → ∃𝑛 ∈ ℕ ((1 − 𝐸) < (1 − (𝐵𝑛)) ∧ (1 / (𝐴𝑛)) < 𝐸))
Distinct variable groups:   𝑖,𝑛,𝐴   𝐵,𝑖,𝑛   𝑖,𝐸,𝑛   𝜑,𝑖,𝑛   𝑛,𝐹   𝑛,𝐺
Allowed substitution hints:   𝐹(𝑖)   𝐺(𝑖)

Proof of Theorem stoweidlem7
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 nnuz 12095 . . . . 5 ℕ = (ℤ‘1)
2 1zzd 11826 . . . . 5 (𝜑 → 1 ∈ ℤ)
3 stoweidlem7.7 . . . . 5 (𝜑𝐸 ∈ ℝ+)
4 stoweidlem7.2 . . . . . 6 𝐺 = (𝑖 ∈ ℕ0 ↦ (𝐵𝑖))
5 oveq2 6984 . . . . . 6 (𝑖 = 𝑘 → (𝐵𝑖) = (𝐵𝑘))
6 nnnn0 11715 . . . . . . 7 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
76adantl 474 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ0)
8 stoweidlem7.5 . . . . . . . . 9 (𝜑𝐵 ∈ ℝ+)
98rpcnd 12250 . . . . . . . 8 (𝜑𝐵 ∈ ℂ)
109adantr 473 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → 𝐵 ∈ ℂ)
1110, 7expcld 13325 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (𝐵𝑘) ∈ ℂ)
124, 5, 7, 11fvmptd3 6617 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) = (𝐵𝑘))
13 1red 10440 . . . . . . . . . 10 (𝜑 → 1 ∈ ℝ)
1413renegcld 10868 . . . . . . . . 9 (𝜑 → -1 ∈ ℝ)
15 0red 10443 . . . . . . . . 9 (𝜑 → 0 ∈ ℝ)
168rpred 12248 . . . . . . . . 9 (𝜑𝐵 ∈ ℝ)
17 neg1lt0 11564 . . . . . . . . . 10 -1 < 0
1817a1i 11 . . . . . . . . 9 (𝜑 → -1 < 0)
198rpgt0d 12251 . . . . . . . . 9 (𝜑 → 0 < 𝐵)
2014, 15, 16, 18, 19lttrd 10601 . . . . . . . 8 (𝜑 → -1 < 𝐵)
21 stoweidlem7.6 . . . . . . . 8 (𝜑𝐵 < 1)
2216, 13absltd 14650 . . . . . . . 8 (𝜑 → ((abs‘𝐵) < 1 ↔ (-1 < 𝐵𝐵 < 1)))
2320, 21, 22mpbir2and 700 . . . . . . 7 (𝜑 → (abs‘𝐵) < 1)
249, 23expcnv 15079 . . . . . 6 (𝜑 → (𝑖 ∈ ℕ0 ↦ (𝐵𝑖)) ⇝ 0)
254, 24syl5eqbr 4964 . . . . 5 (𝜑𝐺 ⇝ 0)
261, 2, 3, 12, 25climi 14728 . . . 4 (𝜑 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸))
27 r19.26 3121 . . . . . . . . . . . . . 14 (∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸) ↔ (∀𝑘 ∈ (ℤ𝑛)(𝐵𝑘) ∈ ℂ ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘((𝐵𝑘) − 0)) < 𝐸))
2827simprbi 489 . . . . . . . . . . . . 13 (∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸) → ∀𝑘 ∈ (ℤ𝑛)(abs‘((𝐵𝑘) − 0)) < 𝐸)
2928ad2antlr 714 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ𝑛)) → ∀𝑘 ∈ (ℤ𝑛)(abs‘((𝐵𝑘) − 0)) < 𝐸)
30 oveq2 6984 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑖 → (𝐵𝑘) = (𝐵𝑖))
3130oveq1d 6991 . . . . . . . . . . . . . . 15 (𝑘 = 𝑖 → ((𝐵𝑘) − 0) = ((𝐵𝑖) − 0))
3231fveq2d 6503 . . . . . . . . . . . . . 14 (𝑘 = 𝑖 → (abs‘((𝐵𝑘) − 0)) = (abs‘((𝐵𝑖) − 0)))
3332breq1d 4939 . . . . . . . . . . . . 13 (𝑘 = 𝑖 → ((abs‘((𝐵𝑘) − 0)) < 𝐸 ↔ (abs‘((𝐵𝑖) − 0)) < 𝐸))
3433rspccva 3535 . . . . . . . . . . . 12 ((∀𝑘 ∈ (ℤ𝑛)(abs‘((𝐵𝑘) − 0)) < 𝐸𝑖 ∈ (ℤ𝑛)) → (abs‘((𝐵𝑖) − 0)) < 𝐸)
3529, 34sylancom 579 . . . . . . . . . . 11 ((((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ𝑛)) → (abs‘((𝐵𝑖) − 0)) < 𝐸)
36 simplll 762 . . . . . . . . . . . . . . 15 ((((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ𝑛)) → 𝜑)
3736, 8syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ𝑛)) → 𝐵 ∈ ℝ+)
3837rpred 12248 . . . . . . . . . . . . 13 ((((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ𝑛)) → 𝐵 ∈ ℝ)
39 simpllr 763 . . . . . . . . . . . . . . 15 ((((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ𝑛)) → 𝑛 ∈ ℕ)
40 nnnn0 11715 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
4139, 40syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ𝑛)) → 𝑛 ∈ ℕ0)
42 eluznn0 12131 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℕ0𝑖 ∈ (ℤ𝑛)) → 𝑖 ∈ ℕ0)
4341, 42sylancom 579 . . . . . . . . . . . . 13 ((((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ𝑛)) → 𝑖 ∈ ℕ0)
4438, 43reexpcld 13342 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ𝑛)) → (𝐵𝑖) ∈ ℝ)
45 rpre 12212 . . . . . . . . . . . . 13 (𝐸 ∈ ℝ+𝐸 ∈ ℝ)
4636, 3, 453syl 18 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ𝑛)) → 𝐸 ∈ ℝ)
47 recn 10425 . . . . . . . . . . . . . . . . 17 ((𝐵𝑖) ∈ ℝ → (𝐵𝑖) ∈ ℂ)
4847subid1d 10787 . . . . . . . . . . . . . . . 16 ((𝐵𝑖) ∈ ℝ → ((𝐵𝑖) − 0) = (𝐵𝑖))
4948adantr 473 . . . . . . . . . . . . . . 15 (((𝐵𝑖) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((𝐵𝑖) − 0) = (𝐵𝑖))
5049fveq2d 6503 . . . . . . . . . . . . . 14 (((𝐵𝑖) ∈ ℝ ∧ 𝐸 ∈ ℝ) → (abs‘((𝐵𝑖) − 0)) = (abs‘(𝐵𝑖)))
5150breq1d 4939 . . . . . . . . . . . . 13 (((𝐵𝑖) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((abs‘((𝐵𝑖) − 0)) < 𝐸 ↔ (abs‘(𝐵𝑖)) < 𝐸))
52 abslt 14535 . . . . . . . . . . . . 13 (((𝐵𝑖) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((abs‘(𝐵𝑖)) < 𝐸 ↔ (-𝐸 < (𝐵𝑖) ∧ (𝐵𝑖) < 𝐸)))
5351, 52bitrd 271 . . . . . . . . . . . 12 (((𝐵𝑖) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((abs‘((𝐵𝑖) − 0)) < 𝐸 ↔ (-𝐸 < (𝐵𝑖) ∧ (𝐵𝑖) < 𝐸)))
5444, 46, 53syl2anc 576 . . . . . . . . . . 11 ((((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ𝑛)) → ((abs‘((𝐵𝑖) − 0)) < 𝐸 ↔ (-𝐸 < (𝐵𝑖) ∧ (𝐵𝑖) < 𝐸)))
5535, 54mpbid 224 . . . . . . . . . 10 ((((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ𝑛)) → (-𝐸 < (𝐵𝑖) ∧ (𝐵𝑖) < 𝐸))
5655simprd 488 . . . . . . . . 9 ((((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ𝑛)) → (𝐵𝑖) < 𝐸)
57 eluznn 12132 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (ℤ𝑛)) → 𝑖 ∈ ℕ)
5839, 57sylancom 579 . . . . . . . . . 10 ((((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ𝑛)) → 𝑖 ∈ ℕ)
5916adantr 473 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → 𝐵 ∈ ℝ)
60 nnnn0 11715 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → 𝑖 ∈ ℕ0)
6160adantl 474 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ0)
6259, 61reexpcld 13342 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → (𝐵𝑖) ∈ ℝ)
633rpred 12248 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℝ)
6463adantr 473 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → 𝐸 ∈ ℝ)
65 1red 10440 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → 1 ∈ ℝ)
6662, 64, 65ltsub2d 11051 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → ((𝐵𝑖) < 𝐸 ↔ (1 − 𝐸) < (1 − (𝐵𝑖))))
6736, 58, 66syl2anc 576 . . . . . . . . 9 ((((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ𝑛)) → ((𝐵𝑖) < 𝐸 ↔ (1 − 𝐸) < (1 − (𝐵𝑖))))
6856, 67mpbid 224 . . . . . . . 8 ((((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ𝑛)) → (1 − 𝐸) < (1 − (𝐵𝑖)))
6968ralrimiva 3133 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸)) → ∀𝑖 ∈ (ℤ𝑛)(1 − 𝐸) < (1 − (𝐵𝑖)))
7030oveq2d 6992 . . . . . . . . 9 (𝑘 = 𝑖 → (1 − (𝐵𝑘)) = (1 − (𝐵𝑖)))
7170breq2d 4941 . . . . . . . 8 (𝑘 = 𝑖 → ((1 − 𝐸) < (1 − (𝐵𝑘)) ↔ (1 − 𝐸) < (1 − (𝐵𝑖))))
7271cbvralv 3384 . . . . . . 7 (∀𝑘 ∈ (ℤ𝑛)(1 − 𝐸) < (1 − (𝐵𝑘)) ↔ ∀𝑖 ∈ (ℤ𝑛)(1 − 𝐸) < (1 − (𝐵𝑖)))
7369, 72sylibr 226 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸)) → ∀𝑘 ∈ (ℤ𝑛)(1 − 𝐸) < (1 − (𝐵𝑘)))
7473ex 405 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸) → ∀𝑘 ∈ (ℤ𝑛)(1 − 𝐸) < (1 − (𝐵𝑘))))
7574reximdva 3220 . . . 4 (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((𝐵𝑘) ∈ ℂ ∧ (abs‘((𝐵𝑘) − 0)) < 𝐸) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)(1 − 𝐸) < (1 − (𝐵𝑘))))
7626, 75mpd 15 . . 3 (𝜑 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)(1 − 𝐸) < (1 − (𝐵𝑘)))
77 stoweidlem7.1 . . . . . 6 𝐹 = (𝑖 ∈ ℕ0 ↦ ((1 / 𝐴)↑𝑖))
78 oveq2 6984 . . . . . 6 (𝑖 = 𝑘 → ((1 / 𝐴)↑𝑖) = ((1 / 𝐴)↑𝑘))
79 stoweidlem7.3 . . . . . . . . . 10 (𝜑𝐴 ∈ ℝ)
8079recnd 10468 . . . . . . . . 9 (𝜑𝐴 ∈ ℂ)
81 0lt1 10963 . . . . . . . . . . . 12 0 < 1
8281a1i 11 . . . . . . . . . . 11 (𝜑 → 0 < 1)
83 stoweidlem7.4 . . . . . . . . . . 11 (𝜑 → 1 < 𝐴)
8415, 13, 79, 82, 83lttrd 10601 . . . . . . . . . 10 (𝜑 → 0 < 𝐴)
8584gt0ne0d 11005 . . . . . . . . 9 (𝜑𝐴 ≠ 0)
8680, 85reccld 11210 . . . . . . . 8 (𝜑 → (1 / 𝐴) ∈ ℂ)
8786adantr 473 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (1 / 𝐴) ∈ ℂ)
8887, 7expcld 13325 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ((1 / 𝐴)↑𝑘) ∈ ℂ)
8977, 78, 7, 88fvmptd3 6617 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) = ((1 / 𝐴)↑𝑘))
9079, 85rereccld 11268 . . . . . . . . 9 (𝜑 → (1 / 𝐴) ∈ ℝ)
9179, 84recgt0d 11375 . . . . . . . . 9 (𝜑 → 0 < (1 / 𝐴))
9214, 15, 90, 18, 91lttrd 10601 . . . . . . . 8 (𝜑 → -1 < (1 / 𝐴))
93 ltdiv23 11332 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (1 ∈ ℝ ∧ 0 < 1)) → ((1 / 𝐴) < 1 ↔ (1 / 1) < 𝐴))
9413, 79, 84, 13, 82, 93syl122anc 1359 . . . . . . . . . 10 (𝜑 → ((1 / 𝐴) < 1 ↔ (1 / 1) < 𝐴))
95 1cnd 10434 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℂ)
9695div1d 11209 . . . . . . . . . . 11 (𝜑 → (1 / 1) = 1)
9796breq1d 4939 . . . . . . . . . 10 (𝜑 → ((1 / 1) < 𝐴 ↔ 1 < 𝐴))
9894, 97bitrd 271 . . . . . . . . 9 (𝜑 → ((1 / 𝐴) < 1 ↔ 1 < 𝐴))
9983, 98mpbird 249 . . . . . . . 8 (𝜑 → (1 / 𝐴) < 1)
10090, 13absltd 14650 . . . . . . . 8 (𝜑 → ((abs‘(1 / 𝐴)) < 1 ↔ (-1 < (1 / 𝐴) ∧ (1 / 𝐴) < 1)))
10192, 99, 100mpbir2and 700 . . . . . . 7 (𝜑 → (abs‘(1 / 𝐴)) < 1)
10286, 101expcnv 15079 . . . . . 6 (𝜑 → (𝑖 ∈ ℕ0 ↦ ((1 / 𝐴)↑𝑖)) ⇝ 0)
10377, 102syl5eqbr 4964 . . . . 5 (𝜑𝐹 ⇝ 0)
1041, 2, 3, 89, 103climi2 14729 . . . 4 (𝜑 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)(abs‘(((1 / 𝐴)↑𝑘) − 0)) < 𝐸)
105 simpll 754 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝜑)
106 uznnssnn 12109 . . . . . . . . 9 (𝑛 ∈ ℕ → (ℤ𝑛) ⊆ ℕ)
107106ad2antlr 714 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (ℤ𝑛) ⊆ ℕ)
108 simpr 477 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑘 ∈ (ℤ𝑛))
109107, 108sseldd 3860 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑘 ∈ ℕ)
11088subid1d 10787 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (((1 / 𝐴)↑𝑘) − 0) = ((1 / 𝐴)↑𝑘))
111110fveq2d 6503 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (abs‘(((1 / 𝐴)↑𝑘) − 0)) = (abs‘((1 / 𝐴)↑𝑘)))
11290adantr 473 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (1 / 𝐴) ∈ ℝ)
113112, 7reexpcld 13342 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ((1 / 𝐴)↑𝑘) ∈ ℝ)
11415, 90, 91ltled 10588 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ (1 / 𝐴))
115114adantr 473 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → 0 ≤ (1 / 𝐴))
116112, 7, 115expge0d 13343 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → 0 ≤ ((1 / 𝐴)↑𝑘))
117113, 116absidd 14643 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (abs‘((1 / 𝐴)↑𝑘)) = ((1 / 𝐴)↑𝑘))
118111, 117eqtrd 2815 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (abs‘(((1 / 𝐴)↑𝑘) − 0)) = ((1 / 𝐴)↑𝑘))
119118breq1d 4939 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ((abs‘(((1 / 𝐴)↑𝑘) − 0)) < 𝐸 ↔ ((1 / 𝐴)↑𝑘) < 𝐸))
120119biimpd 221 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ((abs‘(((1 / 𝐴)↑𝑘) − 0)) < 𝐸 → ((1 / 𝐴)↑𝑘) < 𝐸))
121105, 109, 120syl2anc 576 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((abs‘(((1 / 𝐴)↑𝑘) − 0)) < 𝐸 → ((1 / 𝐴)↑𝑘) < 𝐸))
122121ralimdva 3128 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (∀𝑘 ∈ (ℤ𝑛)(abs‘(((1 / 𝐴)↑𝑘) − 0)) < 𝐸 → ∀𝑘 ∈ (ℤ𝑛)((1 / 𝐴)↑𝑘) < 𝐸))
123122reximdva 3220 . . . 4 (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)(abs‘(((1 / 𝐴)↑𝑘) − 0)) < 𝐸 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((1 / 𝐴)↑𝑘) < 𝐸))
124104, 123mpd 15 . . 3 (𝜑 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((1 / 𝐴)↑𝑘) < 𝐸)
1251rexanuz2 14570 . . 3 (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((1 − 𝐸) < (1 − (𝐵𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸) ↔ (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)(1 − 𝐸) < (1 − (𝐵𝑘)) ∧ ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((1 / 𝐴)↑𝑘) < 𝐸))
12676, 124, 125sylanbrc 575 . 2 (𝜑 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((1 − 𝐸) < (1 − (𝐵𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸))
127 simpr 477 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((1 − 𝐸) < (1 − (𝐵𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) → ∀𝑘 ∈ (ℤ𝑛)((1 − 𝐸) < (1 − (𝐵𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸))
128 nnz 11817 . . . . . . . 8 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
129 uzid 12073 . . . . . . . 8 (𝑛 ∈ ℤ → 𝑛 ∈ (ℤ𝑛))
130128, 129syl 17 . . . . . . 7 (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ𝑛))
131130ad2antlr 714 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((1 − 𝐸) < (1 − (𝐵𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) → 𝑛 ∈ (ℤ𝑛))
132 oveq2 6984 . . . . . . . . . 10 (𝑘 = 𝑛 → (𝐵𝑘) = (𝐵𝑛))
133132oveq2d 6992 . . . . . . . . 9 (𝑘 = 𝑛 → (1 − (𝐵𝑘)) = (1 − (𝐵𝑛)))
134133breq2d 4941 . . . . . . . 8 (𝑘 = 𝑛 → ((1 − 𝐸) < (1 − (𝐵𝑘)) ↔ (1 − 𝐸) < (1 − (𝐵𝑛))))
135 oveq2 6984 . . . . . . . . 9 (𝑘 = 𝑛 → ((1 / 𝐴)↑𝑘) = ((1 / 𝐴)↑𝑛))
136135breq1d 4939 . . . . . . . 8 (𝑘 = 𝑛 → (((1 / 𝐴)↑𝑘) < 𝐸 ↔ ((1 / 𝐴)↑𝑛) < 𝐸))
137134, 136anbi12d 621 . . . . . . 7 (𝑘 = 𝑛 → (((1 − 𝐸) < (1 − (𝐵𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸) ↔ ((1 − 𝐸) < (1 − (𝐵𝑛)) ∧ ((1 / 𝐴)↑𝑛) < 𝐸)))
138137rspccva 3535 . . . . . 6 ((∀𝑘 ∈ (ℤ𝑛)((1 − 𝐸) < (1 − (𝐵𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸) ∧ 𝑛 ∈ (ℤ𝑛)) → ((1 − 𝐸) < (1 − (𝐵𝑛)) ∧ ((1 / 𝐴)↑𝑛) < 𝐸))
139127, 131, 138syl2anc 576 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((1 − 𝐸) < (1 − (𝐵𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) → ((1 − 𝐸) < (1 − (𝐵𝑛)) ∧ ((1 / 𝐴)↑𝑛) < 𝐸))
140 1cnd 10434 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → 1 ∈ ℂ)
14180, 85jca 504 . . . . . . . . . . 11 (𝜑 → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))
142141adantr 473 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))
14340adantl 474 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0)
144 expdiv 13295 . . . . . . . . . 10 ((1 ∈ ℂ ∧ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝑛 ∈ ℕ0) → ((1 / 𝐴)↑𝑛) = ((1↑𝑛) / (𝐴𝑛)))
145140, 142, 143, 144syl3anc 1351 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((1 / 𝐴)↑𝑛) = ((1↑𝑛) / (𝐴𝑛)))
146128adantl 474 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℤ)
147 1exp 13273 . . . . . . . . . . 11 (𝑛 ∈ ℤ → (1↑𝑛) = 1)
148146, 147syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (1↑𝑛) = 1)
149148oveq1d 6991 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((1↑𝑛) / (𝐴𝑛)) = (1 / (𝐴𝑛)))
150145, 149eqtrd 2815 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ((1 / 𝐴)↑𝑛) = (1 / (𝐴𝑛)))
151150breq1d 4939 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (((1 / 𝐴)↑𝑛) < 𝐸 ↔ (1 / (𝐴𝑛)) < 𝐸))
152151adantr 473 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((1 − 𝐸) < (1 − (𝐵𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) → (((1 / 𝐴)↑𝑛) < 𝐸 ↔ (1 / (𝐴𝑛)) < 𝐸))
153152anbi2d 619 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((1 − 𝐸) < (1 − (𝐵𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) → (((1 − 𝐸) < (1 − (𝐵𝑛)) ∧ ((1 / 𝐴)↑𝑛) < 𝐸) ↔ ((1 − 𝐸) < (1 − (𝐵𝑛)) ∧ (1 / (𝐴𝑛)) < 𝐸)))
154139, 153mpbid 224 . . . 4 (((𝜑𝑛 ∈ ℕ) ∧ ∀𝑘 ∈ (ℤ𝑛)((1 − 𝐸) < (1 − (𝐵𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) → ((1 − 𝐸) < (1 − (𝐵𝑛)) ∧ (1 / (𝐴𝑛)) < 𝐸))
155154ex 405 . . 3 ((𝜑𝑛 ∈ ℕ) → (∀𝑘 ∈ (ℤ𝑛)((1 − 𝐸) < (1 − (𝐵𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸) → ((1 − 𝐸) < (1 − (𝐵𝑛)) ∧ (1 / (𝐴𝑛)) < 𝐸)))
156155reximdva 3220 . 2 (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((1 − 𝐸) < (1 − (𝐵𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸) → ∃𝑛 ∈ ℕ ((1 − 𝐸) < (1 − (𝐵𝑛)) ∧ (1 / (𝐴𝑛)) < 𝐸)))
157126, 156mpd 15 1 (𝜑 → ∃𝑛 ∈ ℕ ((1 − 𝐸) < (1 − (𝐵𝑛)) ∧ (1 / (𝐴𝑛)) < 𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387   = wceq 1507  wcel 2050  wne 2968  wral 3089  wrex 3090  wss 3830   class class class wbr 4929  cmpt 5008  cfv 6188  (class class class)co 6976  cc 10333  cr 10334  0cc0 10335  1c1 10336   < clt 10474  cle 10475  cmin 10670  -cneg 10671   / cdiv 11098  cn 11439  0cn0 11707  cz 11793  cuz 12058  +crp 12204  cexp 13244  abscabs 14454  cli 14702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2751  ax-rep 5049  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-cnex 10391  ax-resscn 10392  ax-1cn 10393  ax-icn 10394  ax-addcl 10395  ax-addrcl 10396  ax-mulcl 10397  ax-mulrcl 10398  ax-mulcom 10399  ax-addass 10400  ax-mulass 10401  ax-distr 10402  ax-i2m1 10403  ax-1ne0 10404  ax-1rid 10405  ax-rnegex 10406  ax-rrecex 10407  ax-cnre 10408  ax-pre-lttri 10409  ax-pre-lttrn 10410  ax-pre-ltadd 10411  ax-pre-mulgt0 10412  ax-pre-sup 10413
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3418  df-sbc 3683  df-csb 3788  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-pss 3846  df-nul 4180  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-riota 6937  df-ov 6979  df-oprab 6980  df-mpo 6981  df-om 7397  df-2nd 7502  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-er 8089  df-pm 8209  df-en 8307  df-dom 8308  df-sdom 8309  df-sup 8701  df-inf 8702  df-pnf 10476  df-mnf 10477  df-xr 10478  df-ltxr 10479  df-le 10480  df-sub 10672  df-neg 10673  df-div 11099  df-nn 11440  df-2 11503  df-3 11504  df-n0 11708  df-z 11794  df-uz 12059  df-rp 12205  df-fl 12977  df-seq 13185  df-exp 13245  df-cj 14319  df-re 14320  df-im 14321  df-sqrt 14455  df-abs 14456  df-clim 14706  df-rlim 14707
This theorem is referenced by:  stoweidlem49  41763
  Copyright terms: Public domain W3C validator