Step | Hyp | Ref
| Expression |
1 | | axcaucvg.n |
. . . 4
⊢ 𝑁 = ∩
{𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} |
2 | | axcaucvg.f |
. . . 4
⊢ (𝜑 → 𝐹:𝑁⟶ℝ) |
3 | | axcaucvg.cau |
. . . 4
⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1))))) |
4 | | axcaucvg.g |
. . . 4
⊢ 𝐺 = (𝑗 ∈ N ↦
(℩𝑧 ∈
R (𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑗, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑗, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) = 〈𝑧,
0R〉)) |
5 | 1, 2, 3, 4 | axcaucvglemf 7062 |
. . 3
⊢ (𝜑 → 𝐺:N⟶R) |
6 | 1, 2, 3, 4 | axcaucvglemcau 7064 |
. . 3
⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N
𝑘 → ((𝐺‘𝑛) <R ((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ∧ (𝐺‘𝑘) <R ((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R )))) |
7 | 5, 6 | caucvgsr 6978 |
. 2
⊢ (𝜑 → ∃𝑏 ∈ R ∀𝑎 ∈ R
(0R <R 𝑎 → ∃𝑐 ∈ N ∀𝑘 ∈ N (𝑐 <N
𝑘 → ((𝐺‘𝑘) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑘) +R 𝑎))))) |
8 | | opelreal 6996 |
. . . . 5
⊢
(〈𝑏,
0R〉 ∈ ℝ ↔ 𝑏 ∈ R) |
9 | 8 | biimpri 131 |
. . . 4
⊢ (𝑏 ∈ R →
〈𝑏,
0R〉 ∈ ℝ) |
10 | 9 | ad2antrl 473 |
. . 3
⊢ ((𝜑 ∧ (𝑏 ∈ R ∧ ∀𝑎 ∈ R
(0R <R 𝑎 → ∃𝑐 ∈ N ∀𝑘 ∈ N (𝑐 <N
𝑘 → ((𝐺‘𝑘) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑘) +R 𝑎)))))) → 〈𝑏,
0R〉 ∈ ℝ) |
11 | | breq2 3789 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑘 → (𝑐 <N 𝑑 ↔ 𝑐 <N 𝑘)) |
12 | | fveq2 5198 |
. . . . . . . . . . . 12
⊢ (𝑑 = 𝑘 → (𝐺‘𝑑) = (𝐺‘𝑘)) |
13 | 12 | breq1d 3795 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑘 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ↔ (𝐺‘𝑘) <R (𝑏 +R
𝑎))) |
14 | 12 | oveq1d 5547 |
. . . . . . . . . . . 12
⊢ (𝑑 = 𝑘 → ((𝐺‘𝑑) +R 𝑎) = ((𝐺‘𝑘) +R 𝑎)) |
15 | 14 | breq2d 3797 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑘 → (𝑏 <R ((𝐺‘𝑑) +R 𝑎) ↔ 𝑏 <R ((𝐺‘𝑘) +R 𝑎))) |
16 | 13, 15 | anbi12d 456 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑘 → (((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)) ↔ ((𝐺‘𝑘) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑘) +R 𝑎)))) |
17 | 11, 16 | imbi12d 232 |
. . . . . . . . 9
⊢ (𝑑 = 𝑘 → ((𝑐 <N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎))) ↔ (𝑐 <N 𝑘 → ((𝐺‘𝑘) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑘) +R 𝑎))))) |
18 | 17 | cbvralv 2577 |
. . . . . . . 8
⊢
(∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎))) ↔ ∀𝑘 ∈ N (𝑐 <N
𝑘 → ((𝐺‘𝑘) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑘) +R 𝑎)))) |
19 | 18 | rexbii 2373 |
. . . . . . 7
⊢
(∃𝑐 ∈
N ∀𝑑
∈ N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎))) ↔ ∃𝑐 ∈ N
∀𝑘 ∈
N (𝑐
<N 𝑘 → ((𝐺‘𝑘) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑘) +R 𝑎)))) |
20 | 19 | imbi2i 224 |
. . . . . 6
⊢
((0R <R 𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))) ↔
(0R <R 𝑎 → ∃𝑐 ∈ N ∀𝑘 ∈ N (𝑐 <N
𝑘 → ((𝐺‘𝑘) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑘) +R 𝑎))))) |
21 | 20 | ralbii 2372 |
. . . . 5
⊢
(∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))) ↔ ∀𝑎 ∈ R
(0R <R 𝑎 → ∃𝑐 ∈ N ∀𝑘 ∈ N (𝑐 <N
𝑘 → ((𝐺‘𝑘) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑘) +R 𝑎))))) |
22 | 21 | anbi2i 444 |
. . . 4
⊢ ((𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎))))) ↔ (𝑏 ∈ R ∧ ∀𝑎 ∈ R
(0R <R 𝑎 → ∃𝑐 ∈ N ∀𝑘 ∈ N (𝑐 <N
𝑘 → ((𝐺‘𝑘) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑘) +R 𝑎)))))) |
23 | | elreal 6997 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ ↔
∃𝑒 ∈
R 〈𝑒,
0R〉 = 𝑥) |
24 | 23 | biimpi 118 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ →
∃𝑒 ∈
R 〈𝑒,
0R〉 = 𝑥) |
25 | 24 | ad2antlr 472 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑏 ∈ R ∧ ∀𝑎 ∈ R
(0R <R 𝑎 → ∃𝑐 ∈ N ∀𝑑 ∈ N (𝑐 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
→ ∃𝑒 ∈
R 〈𝑒,
0R〉 = 𝑥) |
26 | | simplrr 502 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑏 ∈ R ∧ ∀𝑎 ∈ R
(0R <R 𝑎 → ∃𝑐 ∈ N ∀𝑑 ∈ N (𝑐 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) → ∀𝑎 ∈ R
(0R <R 𝑎 → ∃𝑐 ∈ N ∀𝑑 ∈ N (𝑐 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎))))) |
27 | 26 | ad2antrr 471 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) → ∀𝑎 ∈ R
(0R <R 𝑎 → ∃𝑐 ∈ N ∀𝑑 ∈ N (𝑐 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎))))) |
28 | | simprr 498 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) → 〈𝑒,
0R〉 = 𝑥) |
29 | | simplr 496 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) → 0
<ℝ 𝑥) |
30 | | df-0 6988 |
. . . . . . . . . . . . . . 15
⊢ 0 =
〈0R,
0R〉 |
31 | 30 | breq1i 3792 |
. . . . . . . . . . . . . 14
⊢ (0
<ℝ 〈𝑒, 0R〉 ↔
〈0R, 0R〉
<ℝ 〈𝑒,
0R〉) |
32 | | ltresr 7007 |
. . . . . . . . . . . . . 14
⊢
(〈0R, 0R〉
<ℝ 〈𝑒, 0R〉 ↔
0R <R 𝑒) |
33 | 31, 32 | bitri 182 |
. . . . . . . . . . . . 13
⊢ (0
<ℝ 〈𝑒, 0R〉 ↔
0R <R 𝑒) |
34 | | breq2 3789 |
. . . . . . . . . . . . 13
⊢
(〈𝑒,
0R〉 = 𝑥 → (0 <ℝ 〈𝑒,
0R〉 ↔ 0 <ℝ 𝑥)) |
35 | 33, 34 | syl5rbbr 193 |
. . . . . . . . . . . 12
⊢
(〈𝑒,
0R〉 = 𝑥 → (0 <ℝ 𝑥 ↔
0R <R 𝑒)) |
36 | 35 | biimpa 290 |
. . . . . . . . . . 11
⊢
((〈𝑒,
0R〉 = 𝑥 ∧ 0 <ℝ 𝑥) →
0R <R 𝑒) |
37 | 28, 29, 36 | syl2anc 403 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) →
0R <R 𝑒) |
38 | | breq2 3789 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑒 → (0R
<R 𝑎 ↔ 0R
<R 𝑒)) |
39 | | oveq2 5540 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑒 → (𝑏 +R 𝑎) = (𝑏 +R 𝑒)) |
40 | 39 | breq2d 3797 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑒 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ↔ (𝐺‘𝑑) <R (𝑏 +R
𝑒))) |
41 | | oveq2 5540 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑒 → ((𝐺‘𝑑) +R 𝑎) = ((𝐺‘𝑑) +R 𝑒)) |
42 | 41 | breq2d 3797 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑒 → (𝑏 <R ((𝐺‘𝑑) +R 𝑎) ↔ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))) |
43 | 40, 42 | anbi12d 456 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑒 → (((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)) ↔ ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒)))) |
44 | 43 | imbi2d 228 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑒 → ((𝑐 <N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎))) ↔ (𝑐 <N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) |
45 | 44 | rexralbidv 2392 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑒 → (∃𝑐 ∈ N ∀𝑑 ∈ N (𝑐 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎))) ↔ ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) |
46 | 38, 45 | imbi12d 232 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑒 → ((0R
<R 𝑎 → ∃𝑐 ∈ N ∀𝑑 ∈ N (𝑐 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))) ↔
(0R <R 𝑒 → ∃𝑐 ∈ N ∀𝑑 ∈ N (𝑐 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒)))))) |
47 | 46 | rspcv 2697 |
. . . . . . . . . . 11
⊢ (𝑒 ∈ R →
(∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))) →
(0R <R 𝑒 → ∃𝑐 ∈ N ∀𝑑 ∈ N (𝑐 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒)))))) |
48 | 47 | ad2antrl 473 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) → (∀𝑎 ∈ R
(0R <R 𝑎 → ∃𝑐 ∈ N ∀𝑑 ∈ N (𝑐 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))) →
(0R <R 𝑒 → ∃𝑐 ∈ N ∀𝑑 ∈ N (𝑐 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒)))))) |
49 | 27, 37, 48 | mp2d 46 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒)))) |
50 | | breq1 3788 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑓 → (𝑐 <N 𝑑 ↔ 𝑓 <N 𝑑)) |
51 | 50 | imbi1d 229 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑓 → ((𝑐 <N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))) ↔ (𝑓 <N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) |
52 | 51 | ralbidv 2368 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑓 → (∀𝑑 ∈ N (𝑐 <N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))) ↔ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) |
53 | 52 | cbvrexv 2578 |
. . . . . . . . 9
⊢
(∃𝑐 ∈
N ∀𝑑
∈ N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))) ↔ ∃𝑓 ∈ N
∀𝑑 ∈
N (𝑓
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒)))) |
54 | 49, 53 | sylib 120 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) → ∃𝑓 ∈ N
∀𝑑 ∈
N (𝑓
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒)))) |
55 | | pitonn 7016 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ N →
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑓, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑓, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 ∈ ∩ {𝑥
∣ (1 ∈ 𝑥 ∧
∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}) |
56 | 55, 1 | syl6eleqr 2172 |
. . . . . . . . . 10
⊢ (𝑓 ∈ N →
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑓, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑓, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 ∈ 𝑁) |
57 | 56 | ad2antrl 473 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) →
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑓, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑓, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 ∈ 𝑁) |
58 | 1 | nntopi 7060 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝑁 → ∃𝑔 ∈ N
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘) |
59 | 58 | adantl 271 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) → ∃𝑔 ∈ N
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘) |
60 | | simprl 497 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → 𝑔 ∈ N) |
61 | | simplrr 502 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) → ∀𝑑 ∈ N (𝑓 <N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒)))) |
62 | 61 | adantr 270 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒)))) |
63 | | breq2 3789 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = 𝑔 → (𝑓 <N 𝑑 ↔ 𝑓 <N 𝑔)) |
64 | | fveq2 5198 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 = 𝑔 → (𝐺‘𝑑) = (𝐺‘𝑔)) |
65 | 64 | breq1d 3795 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = 𝑔 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ↔ (𝐺‘𝑔) <R (𝑏 +R
𝑒))) |
66 | 64 | oveq1d 5547 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 = 𝑔 → ((𝐺‘𝑑) +R 𝑒) = ((𝐺‘𝑔) +R 𝑒)) |
67 | 66 | breq2d 3797 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = 𝑔 → (𝑏 <R ((𝐺‘𝑑) +R 𝑒) ↔ 𝑏 <R ((𝐺‘𝑔) +R 𝑒))) |
68 | 65, 67 | anbi12d 456 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = 𝑔 → (((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒)) ↔ ((𝐺‘𝑔) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑔) +R 𝑒)))) |
69 | 63, 68 | imbi12d 232 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = 𝑔 → ((𝑓 <N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))) ↔ (𝑓 <N 𝑔 → ((𝐺‘𝑔) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑔) +R 𝑒))))) |
70 | 69 | rspcv 2697 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ N →
(∀𝑑 ∈
N (𝑓
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))) → (𝑓 <N 𝑔 → ((𝐺‘𝑔) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑔) +R 𝑒))))) |
71 | 60, 62, 70 | sylc 61 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → (𝑓 <N 𝑔 → ((𝐺‘𝑔) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑔) +R 𝑒)))) |
72 | | simplrl 501 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) → 𝑓 ∈ N) |
73 | 72 | adantr 270 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → 𝑓 ∈ N) |
74 | | ltrennb 7022 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ N ∧
𝑔 ∈ N)
→ (𝑓
<N 𝑔 ↔ 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑓, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑓, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉
<ℝ 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R ,
0R〉)) |
75 | 73, 60, 74 | syl2anc 403 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → (𝑓 <N 𝑔 ↔
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑓, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑓, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉
<ℝ 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R ,
0R〉)) |
76 | | simprr 498 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) →
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘) |
77 | 76 | breq2d 3797 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) →
(〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑓, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑓, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉
<ℝ 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 ↔
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑓, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑓, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉
<ℝ 𝑘)) |
78 | 75, 77 | bitrd 186 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → (𝑓 <N 𝑔 ↔
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑓, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑓, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉
<ℝ 𝑘)) |
79 | | ltresr 7007 |
. . . . . . . . . . . . . 14
⊢
(〈(𝐺‘𝑔), 0R〉
<ℝ 〈(𝑏 +R 𝑒),
0R〉 ↔ (𝐺‘𝑔) <R (𝑏 +R
𝑒)) |
80 | | simplll 499 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑏 ∈ R ∧ ∀𝑎 ∈ R
(0R <R 𝑎 → ∃𝑐 ∈ N ∀𝑑 ∈ N (𝑐 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
→ 𝜑) |
81 | 80 | ad4antr 477 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → 𝜑) |
82 | 1, 2, 3, 4 | axcaucvglemval 7063 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑔 ∈ N) → (𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) = 〈(𝐺‘𝑔),
0R〉) |
83 | 81, 60, 82 | syl2anc 403 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → (𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) = 〈(𝐺‘𝑔),
0R〉) |
84 | 76 | fveq2d 5202 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → (𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) = (𝐹‘𝑘)) |
85 | 83, 84 | eqtr3d 2115 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → 〈(𝐺‘𝑔), 0R〉 = (𝐹‘𝑘)) |
86 | | simplrl 501 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑏 ∈ R ∧ ∀𝑎 ∈ R
(0R <R 𝑎 → ∃𝑐 ∈ N ∀𝑑 ∈ N (𝑐 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) → 𝑏 ∈ R) |
87 | 86 | ad5antr 479 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → 𝑏 ∈ R) |
88 | | simplrl 501 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) → 𝑒 ∈ R) |
89 | 88 | ad2antrr 471 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → 𝑒 ∈ R) |
90 | | addresr 7005 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑏 ∈ R ∧
𝑒 ∈ R)
→ (〈𝑏,
0R〉 + 〈𝑒, 0R〉) =
〈(𝑏
+R 𝑒),
0R〉) |
91 | 87, 89, 90 | syl2anc 403 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → (〈𝑏,
0R〉 + 〈𝑒, 0R〉) =
〈(𝑏
+R 𝑒),
0R〉) |
92 | 28 | oveq2d 5548 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) → (〈𝑏,
0R〉 + 〈𝑒, 0R〉) =
(〈𝑏,
0R〉 + 𝑥)) |
93 | 92 | ad3antrrr 475 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → (〈𝑏,
0R〉 + 〈𝑒, 0R〉) =
(〈𝑏,
0R〉 + 𝑥)) |
94 | 91, 93 | eqtr3d 2115 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → 〈(𝑏 +R
𝑒),
0R〉 = (〈𝑏, 0R〉 + 𝑥)) |
95 | 85, 94 | breq12d 3798 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → (〈(𝐺‘𝑔), 0R〉
<ℝ 〈(𝑏 +R 𝑒),
0R〉 ↔ (𝐹‘𝑘) <ℝ (〈𝑏,
0R〉 + 𝑥))) |
96 | 79, 95 | syl5bbr 192 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → ((𝐺‘𝑔) <R (𝑏 +R
𝑒) ↔ (𝐹‘𝑘) <ℝ (〈𝑏,
0R〉 + 𝑥))) |
97 | | ltresr 7007 |
. . . . . . . . . . . . . 14
⊢
(〈𝑏,
0R〉 <ℝ 〈((𝐺‘𝑔) +R 𝑒),
0R〉 ↔ 𝑏 <R ((𝐺‘𝑔) +R 𝑒)) |
98 | 81, 5 | syl 14 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → 𝐺:N⟶R) |
99 | 98, 60 | ffvelrnd 5324 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → (𝐺‘𝑔) ∈ R) |
100 | | addresr 7005 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺‘𝑔) ∈ R ∧ 𝑒 ∈ R) →
(〈(𝐺‘𝑔),
0R〉 + 〈𝑒, 0R〉) =
〈((𝐺‘𝑔) +R
𝑒),
0R〉) |
101 | 99, 89, 100 | syl2anc 403 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → (〈(𝐺‘𝑔), 0R〉 +
〈𝑒,
0R〉) = 〈((𝐺‘𝑔) +R 𝑒),
0R〉) |
102 | 28 | ad3antrrr 475 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → 〈𝑒,
0R〉 = 𝑥) |
103 | 85, 102 | oveq12d 5550 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → (〈(𝐺‘𝑔), 0R〉 +
〈𝑒,
0R〉) = ((𝐹‘𝑘) + 𝑥)) |
104 | 101, 103 | eqtr3d 2115 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → 〈((𝐺‘𝑔) +R 𝑒),
0R〉 = ((𝐹‘𝑘) + 𝑥)) |
105 | 104 | breq2d 3797 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → (〈𝑏,
0R〉 <ℝ 〈((𝐺‘𝑔) +R 𝑒),
0R〉 ↔ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥))) |
106 | 97, 105 | syl5bbr 192 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → (𝑏 <R ((𝐺‘𝑔) +R 𝑒) ↔ 〈𝑏,
0R〉 <ℝ ((𝐹‘𝑘) + 𝑥))) |
107 | 96, 106 | anbi12d 456 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) → (((𝐺‘𝑔) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑔) +R 𝑒)) ↔ ((𝐹‘𝑘) <ℝ (〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥)))) |
108 | 71, 78, 107 | 3imtr3d 200 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) ∧ (𝑔 ∈ N ∧
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑔, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑔, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 = 𝑘)) →
(〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑓, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑓, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉
<ℝ 𝑘
→ ((𝐹‘𝑘) <ℝ
(〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥)))) |
109 | 59, 108 | rexlimddv 2481 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) ∧ 𝑘 ∈ 𝑁) → (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑓, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑓, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉
<ℝ 𝑘
→ ((𝐹‘𝑘) <ℝ
(〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥)))) |
110 | 109 | ralrimiva 2434 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) → ∀𝑘 ∈ 𝑁 (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑓, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑓, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉
<ℝ 𝑘
→ ((𝐹‘𝑘) <ℝ
(〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥)))) |
111 | | breq1 3788 |
. . . . . . . . . . . 12
⊢ (𝑗 = 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑓, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑓, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 → (𝑗 <ℝ 𝑘 ↔
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑓, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑓, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉
<ℝ 𝑘)) |
112 | 111 | imbi1d 229 |
. . . . . . . . . . 11
⊢ (𝑗 = 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑓, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑓, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 → ((𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥))) ↔ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑓, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑓, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉
<ℝ 𝑘
→ ((𝐹‘𝑘) <ℝ
(〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥))))) |
113 | 112 | ralbidv 2368 |
. . . . . . . . . 10
⊢ (𝑗 = 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑓, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑓, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 →
(∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥))) ↔ ∀𝑘 ∈ 𝑁 (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑓, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑓, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉
<ℝ 𝑘
→ ((𝐹‘𝑘) <ℝ
(〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥))))) |
114 | 113 | rspcev 2701 |
. . . . . . . . 9
⊢
((〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑓, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑓, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 ∈ 𝑁 ∧ ∀𝑘 ∈ 𝑁 (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑓, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑓, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉
<ℝ 𝑘
→ ((𝐹‘𝑘) <ℝ
(〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥)))) → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥)))) |
115 | 57, 110, 114 | syl2anc 403 |
. . . . . . . 8
⊢
((((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) ∧ (𝑓 ∈ N ∧ ∀𝑑 ∈ N (𝑓 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑒) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑒))))) → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥)))) |
116 | 54, 115 | rexlimddv 2481 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝑏 ∈ R ∧
∀𝑎 ∈
R (0R <R
𝑎 → ∃𝑐 ∈ N
∀𝑑 ∈
N (𝑐
<N 𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
∧ (𝑒 ∈
R ∧ 〈𝑒, 0R〉 = 𝑥)) → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥)))) |
117 | 25, 116 | rexlimddv 2481 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑏 ∈ R ∧ ∀𝑎 ∈ R
(0R <R 𝑎 → ∃𝑐 ∈ N ∀𝑑 ∈ N (𝑐 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) ∧ 0
<ℝ 𝑥)
→ ∃𝑗 ∈
𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥)))) |
118 | 117 | ex 113 |
. . . . 5
⊢ (((𝜑 ∧ (𝑏 ∈ R ∧ ∀𝑎 ∈ R
(0R <R 𝑎 → ∃𝑐 ∈ N ∀𝑑 ∈ N (𝑐 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) ∧ 𝑥 ∈ ℝ) → (0
<ℝ 𝑥
→ ∃𝑗 ∈
𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥))))) |
119 | 118 | ralrimiva 2434 |
. . . 4
⊢ ((𝜑 ∧ (𝑏 ∈ R ∧ ∀𝑎 ∈ R
(0R <R 𝑎 → ∃𝑐 ∈ N ∀𝑑 ∈ N (𝑐 <N
𝑑 → ((𝐺‘𝑑) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑑) +R 𝑎)))))) → ∀𝑥 ∈ ℝ (0
<ℝ 𝑥
→ ∃𝑗 ∈
𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥))))) |
120 | 22, 119 | sylan2br 282 |
. . 3
⊢ ((𝜑 ∧ (𝑏 ∈ R ∧ ∀𝑎 ∈ R
(0R <R 𝑎 → ∃𝑐 ∈ N ∀𝑘 ∈ N (𝑐 <N
𝑘 → ((𝐺‘𝑘) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑘) +R 𝑎)))))) → ∀𝑥 ∈ ℝ (0
<ℝ 𝑥
→ ∃𝑗 ∈
𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥))))) |
121 | | oveq1 5539 |
. . . . . . . . . 10
⊢ (𝑦 = 〈𝑏, 0R〉 →
(𝑦 + 𝑥) = (〈𝑏, 0R〉 + 𝑥)) |
122 | 121 | breq2d 3797 |
. . . . . . . . 9
⊢ (𝑦 = 〈𝑏, 0R〉 →
((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ↔ (𝐹‘𝑘) <ℝ (〈𝑏,
0R〉 + 𝑥))) |
123 | | breq1 3788 |
. . . . . . . . 9
⊢ (𝑦 = 〈𝑏, 0R〉 →
(𝑦 <ℝ
((𝐹‘𝑘) + 𝑥) ↔ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥))) |
124 | 122, 123 | anbi12d 456 |
. . . . . . . 8
⊢ (𝑦 = 〈𝑏, 0R〉 →
(((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥)) ↔ ((𝐹‘𝑘) <ℝ (〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥)))) |
125 | 124 | imbi2d 228 |
. . . . . . 7
⊢ (𝑦 = 〈𝑏, 0R〉 →
((𝑗 <ℝ
𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥))) ↔ (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥))))) |
126 | 125 | rexralbidv 2392 |
. . . . . 6
⊢ (𝑦 = 〈𝑏, 0R〉 →
(∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥))) ↔ ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥))))) |
127 | 126 | imbi2d 228 |
. . . . 5
⊢ (𝑦 = 〈𝑏, 0R〉 →
((0 <ℝ 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥)))) ↔ (0 <ℝ 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥)))))) |
128 | 127 | ralbidv 2368 |
. . . 4
⊢ (𝑦 = 〈𝑏, 0R〉 →
(∀𝑥 ∈ ℝ
(0 <ℝ 𝑥
→ ∃𝑗 ∈
𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥)))) ↔ ∀𝑥 ∈ ℝ (0 <ℝ
𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥)))))) |
129 | 128 | rspcev 2701 |
. . 3
⊢
((〈𝑏,
0R〉 ∈ ℝ ∧ ∀𝑥 ∈ ℝ (0
<ℝ 𝑥
→ ∃𝑗 ∈
𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (〈𝑏,
0R〉 + 𝑥) ∧ 〈𝑏, 0R〉
<ℝ ((𝐹‘𝑘) + 𝑥))))) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 <ℝ
𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥))))) |
130 | 10, 120, 129 | syl2anc 403 |
. 2
⊢ ((𝜑 ∧ (𝑏 ∈ R ∧ ∀𝑎 ∈ R
(0R <R 𝑎 → ∃𝑐 ∈ N ∀𝑘 ∈ N (𝑐 <N
𝑘 → ((𝐺‘𝑘) <R (𝑏 +R
𝑎) ∧ 𝑏 <R ((𝐺‘𝑘) +R 𝑎)))))) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0
<ℝ 𝑥
→ ∃𝑗 ∈
𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥))))) |
131 | 7, 130 | rexlimddv 2481 |
1
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 <ℝ
𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥))))) |