Step | Hyp | Ref
| Expression |
1 | | ltrenn 7023 |
. . . . . . . . . 10
⊢ (𝑛 <N
𝑘 →
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉
<ℝ 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑘, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑘, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R ,
0R〉) |
2 | 1 | adantl 271 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑛 ∈ 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〉) |
3 | | pitonn 7016 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ N →
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑘, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑘, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 ∈ ∩ {𝑥
∣ (1 ∈ 𝑥 ∧
∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}) |
4 | | axcaucvg.n |
. . . . . . . . . . . 12
⊢ 𝑁 = ∩
{𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} |
5 | 3, 4 | syl6eleqr 2172 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ N →
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑘, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑘, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 ∈ 𝑁) |
6 | 5 | ad2antlr 472 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧
𝑛
<N 𝑘) → 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑘, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑘, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 ∈ 𝑁) |
7 | | pitonn 7016 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ N →
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 ∈ ∩ {𝑥
∣ (1 ∈ 𝑥 ∧
∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}) |
8 | 7, 4 | syl6eleqr 2172 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ N →
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 ∈ 𝑁) |
9 | 8 | ad3antlr 476 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧
𝑛
<N 𝑘) → 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 ∈ 𝑁) |
10 | | axcaucvg.cau |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1))))) |
11 | | breq1 3788 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑎 → (𝑛 <ℝ 𝑘 ↔ 𝑎 <ℝ 𝑘)) |
12 | | fveq2 5198 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑎 → (𝐹‘𝑛) = (𝐹‘𝑎)) |
13 | | oveq1 5539 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑎 → (𝑛 · 𝑟) = (𝑎 · 𝑟)) |
14 | 13 | eqeq1d 2089 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑎 → ((𝑛 · 𝑟) = 1 ↔ (𝑎 · 𝑟) = 1)) |
15 | 14 | riotabidv 5490 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑎 → (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1) = (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)) |
16 | 15 | oveq2d 5548 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑎 → ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) = ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1))) |
17 | 12, 16 | breq12d 3798 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑎 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ↔ (𝐹‘𝑎) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)))) |
18 | 12, 15 | oveq12d 5550 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑎 → ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) = ((𝐹‘𝑎) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1))) |
19 | 18 | breq2d 3797 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑎 → ((𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ↔ (𝐹‘𝑘) <ℝ ((𝐹‘𝑎) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)))) |
20 | 17, 19 | anbi12d 456 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑎 → (((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1))) ↔ ((𝐹‘𝑎) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑎) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1))))) |
21 | 11, 20 | imbi12d 232 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑎 → ((𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))) ↔ (𝑎 <ℝ 𝑘 → ((𝐹‘𝑎) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑎) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)))))) |
22 | | breq2 3789 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑏 → (𝑎 <ℝ 𝑘 ↔ 𝑎 <ℝ 𝑏)) |
23 | | fveq2 5198 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑏 → (𝐹‘𝑘) = (𝐹‘𝑏)) |
24 | 23 | oveq1d 5547 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑏 → ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)) = ((𝐹‘𝑏) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1))) |
25 | 24 | breq2d 3797 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑏 → ((𝐹‘𝑎) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)) ↔ (𝐹‘𝑎) <ℝ ((𝐹‘𝑏) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)))) |
26 | 23 | breq1d 3795 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑏 → ((𝐹‘𝑘) <ℝ ((𝐹‘𝑎) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)) ↔ (𝐹‘𝑏) <ℝ ((𝐹‘𝑎) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)))) |
27 | 25, 26 | anbi12d 456 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑏 → (((𝐹‘𝑎) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑎) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1))) ↔ ((𝐹‘𝑎) <ℝ ((𝐹‘𝑏) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)) ∧ (𝐹‘𝑏) <ℝ ((𝐹‘𝑎) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1))))) |
28 | 22, 27 | imbi12d 232 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑏 → ((𝑎 <ℝ 𝑘 → ((𝐹‘𝑎) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑎) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)))) ↔ (𝑎 <ℝ 𝑏 → ((𝐹‘𝑎) <ℝ ((𝐹‘𝑏) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)) ∧ (𝐹‘𝑏) <ℝ ((𝐹‘𝑎) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)))))) |
29 | 21, 28 | cbvral2v 2585 |
. . . . . . . . . . . . 13
⊢
(∀𝑛 ∈
𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))) ↔ ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎 <ℝ 𝑏 → ((𝐹‘𝑎) <ℝ ((𝐹‘𝑏) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)) ∧ (𝐹‘𝑏) <ℝ ((𝐹‘𝑎) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1))))) |
30 | 10, 29 | sylib 120 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎 <ℝ 𝑏 → ((𝐹‘𝑎) <ℝ ((𝐹‘𝑏) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)) ∧ (𝐹‘𝑏) <ℝ ((𝐹‘𝑎) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1))))) |
31 | 30 | ad3antrrr 475 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧
𝑛
<N 𝑘) → ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎 <ℝ 𝑏 → ((𝐹‘𝑎) <ℝ ((𝐹‘𝑏) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)) ∧ (𝐹‘𝑏) <ℝ ((𝐹‘𝑎) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1))))) |
32 | | breq1 3788 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 → (𝑎 <ℝ 𝑏 ↔
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉
<ℝ 𝑏)) |
33 | | fveq2 5198 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 → (𝐹‘𝑎) = (𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R ,
0R〉)) |
34 | | oveq1 5539 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 → (𝑎 · 𝑟) = (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟)) |
35 | 34 | eqeq1d 2089 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 → ((𝑎 · 𝑟) = 1 ↔ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1)) |
36 | 35 | riotabidv 5490 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 →
(℩𝑟 ∈
ℝ (𝑎 · 𝑟) = 1) = (℩𝑟 ∈ ℝ
(〈[〈(〈{𝑙
∣ 𝑙
<Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1)) |
37 | 36 | oveq2d 5548 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 → ((𝐹‘𝑏) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)) = ((𝐹‘𝑏) + (℩𝑟 ∈ ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1))) |
38 | 33, 37 | breq12d 3798 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 → ((𝐹‘𝑎) <ℝ ((𝐹‘𝑏) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)) ↔ (𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉)
<ℝ ((𝐹‘𝑏) + (℩𝑟 ∈ ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1)))) |
39 | 33, 36 | oveq12d 5550 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 → ((𝐹‘𝑎) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)) = ((𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) +
(℩𝑟 ∈
ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1))) |
40 | 39 | breq2d 3797 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 → ((𝐹‘𝑏) <ℝ ((𝐹‘𝑎) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)) ↔ (𝐹‘𝑏) <ℝ ((𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) +
(℩𝑟 ∈
ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1)))) |
41 | 38, 40 | anbi12d 456 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 → (((𝐹‘𝑎) <ℝ ((𝐹‘𝑏) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)) ∧ (𝐹‘𝑏) <ℝ ((𝐹‘𝑎) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1))) ↔ ((𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉)
<ℝ ((𝐹‘𝑏) + (℩𝑟 ∈ ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1)) ∧ (𝐹‘𝑏) <ℝ ((𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) +
(℩𝑟 ∈
ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1))))) |
42 | 32, 41 | imbi12d 232 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 → ((𝑎 <ℝ 𝑏 → ((𝐹‘𝑎) <ℝ ((𝐹‘𝑏) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)) ∧ (𝐹‘𝑏) <ℝ ((𝐹‘𝑎) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)))) ↔ (〈[〈(〈{𝑙 ∣ 𝑙 <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〉 · 𝑟) = 1)) ∧ (𝐹‘𝑏) <ℝ ((𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) +
(℩𝑟 ∈
ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1)))))) |
43 | 42 | ralbidv 2368 |
. . . . . . . . . . . 12
⊢ (𝑎 = 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 →
(∀𝑏 ∈ 𝑁 (𝑎 <ℝ 𝑏 → ((𝐹‘𝑎) <ℝ ((𝐹‘𝑏) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)) ∧ (𝐹‘𝑏) <ℝ ((𝐹‘𝑎) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)))) ↔ ∀𝑏 ∈ 𝑁 (〈[〈(〈{𝑙 ∣ 𝑙 <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〉 · 𝑟) = 1)) ∧ (𝐹‘𝑏) <ℝ ((𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) +
(℩𝑟 ∈
ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1)))))) |
44 | 43 | rspcva 2699 |
. . . . . . . . . . 11
⊢
((〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 ∈ 𝑁 ∧ ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎 <ℝ 𝑏 → ((𝐹‘𝑎) <ℝ ((𝐹‘𝑏) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1)) ∧ (𝐹‘𝑏) <ℝ ((𝐹‘𝑎) + (℩𝑟 ∈ ℝ (𝑎 · 𝑟) = 1))))) → ∀𝑏 ∈ 𝑁 (〈[〈(〈{𝑙 ∣ 𝑙 <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〉 · 𝑟) = 1)) ∧ (𝐹‘𝑏) <ℝ ((𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) +
(℩𝑟 ∈
ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1))))) |
45 | 9, 31, 44 | syl2anc 403 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ 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〉)
<ℝ ((𝐹‘𝑏) + (℩𝑟 ∈ ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1)) ∧ (𝐹‘𝑏) <ℝ ((𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) +
(℩𝑟 ∈
ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1))))) |
46 | | breq2 3789 |
. . . . . . . . . . . 12
⊢ (𝑏 = 〈[〈(〈{𝑙 ∣ 𝑙 <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〉)) |
47 | | fveq2 5198 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑘, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑘, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 → (𝐹‘𝑏) = (𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑘, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑘, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R ,
0R〉)) |
48 | 47 | oveq1d 5547 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑘, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑘, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 → ((𝐹‘𝑏) + (℩𝑟 ∈ ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1)) = ((𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑘, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑘, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) +
(℩𝑟 ∈
ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1))) |
49 | 48 | breq2d 3797 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 〈[〈(〈{𝑙 ∣ 𝑙 <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〉 · 𝑟) = 1)) ↔ (𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <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〉 · 𝑟) = 1)))) |
50 | 47 | breq1d 3795 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 〈[〈(〈{𝑙 ∣ 𝑙 <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〉 · 𝑟) = 1)) ↔ (𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <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〉 · 𝑟) = 1)))) |
51 | 49, 50 | anbi12d 456 |
. . . . . . . . . . . 12
⊢ (𝑏 = 〈[〈(〈{𝑙 ∣ 𝑙 <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〉 · 𝑟) = 1)) ∧ (𝐹‘𝑏) <ℝ ((𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) +
(℩𝑟 ∈
ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1))) ↔ ((𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <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〉 · 𝑟) = 1)) ∧ (𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <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〉 · 𝑟) = 1))))) |
52 | 46, 51 | imbi12d 232 |
. . . . . . . . . . 11
⊢ (𝑏 = 〈[〈(〈{𝑙 ∣ 𝑙 <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〉 · 𝑟) = 1)) ∧ (𝐹‘𝑏) <ℝ ((𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) +
(℩𝑟 ∈
ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1)))) ↔
(〈[〈(〈{𝑙
∣ 𝑙
<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〉) +
(℩𝑟 ∈
ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1)) ∧ (𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <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〉 · 𝑟) = 1)))))) |
53 | 52 | rspcva 2699 |
. . . . . . . . . 10
⊢
((〈[〈(〈{𝑙 ∣ 𝑙 <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〉 · 𝑟) = 1)) ∧ (𝐹‘𝑏) <ℝ ((𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) +
(℩𝑟 ∈
ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1))))) →
(〈[〈(〈{𝑙
∣ 𝑙
<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〉) +
(℩𝑟 ∈
ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1)) ∧ (𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <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〉 · 𝑟) = 1))))) |
54 | 6, 45, 53 | syl2anc 403 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑛 ∈ 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〉 → ((𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <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〉 · 𝑟) = 1)) ∧ (𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <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〉 · 𝑟) = 1))))) |
55 | 2, 54 | mpd 13 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑛 ∈ 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〉) +
(℩𝑟 ∈
ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1)) ∧ (𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <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〉 · 𝑟) = 1)))) |
56 | 55 | simpld 110 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑛 ∈ 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〉) +
(℩𝑟 ∈
ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1))) |
57 | | axcaucvg.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑁⟶ℝ) |
58 | | axcaucvg.g |
. . . . . . . . 9
⊢ 𝐺 = (𝑗 ∈ N ↦
(℩𝑧 ∈
R (𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑗, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑗, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) = 〈𝑧,
0R〉)) |
59 | 4, 57, 10, 58 | axcaucvglemval 7063 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ N) → (𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) = 〈(𝐺‘𝑛),
0R〉) |
60 | 59 | ad2antrr 471 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧
𝑛
<N 𝑘) → (𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) = 〈(𝐺‘𝑛),
0R〉) |
61 | 4, 57, 10, 58 | axcaucvglemval 7063 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ N) → (𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑘, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑘, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) = 〈(𝐺‘𝑘),
0R〉) |
62 | 61 | adantlr 460 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
(𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑘, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑘, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) = 〈(𝐺‘𝑘),
0R〉) |
63 | 62 | adantr 270 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧
𝑛
<N 𝑘) → (𝐹‘〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑘, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑘, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) = 〈(𝐺‘𝑘),
0R〉) |
64 | | recriota 7056 |
. . . . . . . . . 10
⊢ (𝑛 ∈ N →
(℩𝑟 ∈
ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1) =
〈[〈(〈{𝑙
∣ 𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ,
0R〉) |
65 | 64 | ad3antlr 476 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧
𝑛
<N 𝑘) → (℩𝑟 ∈ ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1) =
〈[〈(〈{𝑙
∣ 𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ,
0R〉) |
66 | 63, 65 | oveq12d 5550 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑛 ∈ 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〉 · 𝑟) = 1)) = (〈(𝐺‘𝑘), 0R〉 +
〈[〈(〈{𝑙
∣ 𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ,
0R〉)) |
67 | 4, 57, 10, 58 | axcaucvglemf 7062 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺:N⟶R) |
68 | 67 | ad3antrrr 475 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧
𝑛
<N 𝑘) → 𝐺:N⟶R) |
69 | | simplr 496 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧
𝑛
<N 𝑘) → 𝑘 ∈ N) |
70 | 68, 69 | ffvelrnd 5324 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧
𝑛
<N 𝑘) → (𝐺‘𝑘) ∈ R) |
71 | | recnnpr 6738 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ N →
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 ∈
P) |
72 | | prsrcl 6960 |
. . . . . . . . . . 11
⊢
(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 ∈ P →
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ∈ R) |
73 | 71, 72 | syl 14 |
. . . . . . . . . 10
⊢ (𝑛 ∈ N →
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ∈ R) |
74 | 73 | ad3antlr 476 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧
𝑛
<N 𝑘) → [〈(〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ∈ R) |
75 | | addresr 7005 |
. . . . . . . . 9
⊢ (((𝐺‘𝑘) ∈ R ∧
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ∈ R) → (〈(𝐺‘𝑘), 0R〉 +
〈[〈(〈{𝑙
∣ 𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) =
〈((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ),
0R〉) |
76 | 70, 74, 75 | syl2anc 403 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧
𝑛
<N 𝑘) → (〈(𝐺‘𝑘), 0R〉 +
〈[〈(〈{𝑙
∣ 𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) =
〈((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ),
0R〉) |
77 | 66, 76 | eqtrd 2113 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑛 ∈ 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〉 · 𝑟) = 1)) = 〈((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ),
0R〉) |
78 | 56, 60, 77 | 3brtr3d 3814 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧
𝑛
<N 𝑘) → 〈(𝐺‘𝑛), 0R〉
<ℝ 〈((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ),
0R〉) |
79 | | ltresr 7007 |
. . . . . 6
⊢
(〈(𝐺‘𝑛), 0R〉
<ℝ 〈((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ), 0R〉 ↔ (𝐺‘𝑛) <R ((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R )) |
80 | 78, 79 | sylib 120 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧
𝑛
<N 𝑘) → (𝐺‘𝑛) <R ((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R )) |
81 | 55 | simprd 112 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑛 ∈ 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〉) +
(℩𝑟 ∈
ℝ (〈[〈(〈{𝑙 ∣ 𝑙 <Q [〈𝑛, 1𝑜〉]
~Q }, {𝑢 ∣ [〈𝑛, 1𝑜〉]
~Q <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 · 𝑟) = 1))) |
82 | 60, 65 | oveq12d 5550 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑛 ∈ 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〉 · 𝑟) = 1)) = (〈(𝐺‘𝑛), 0R〉 +
〈[〈(〈{𝑙
∣ 𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ,
0R〉)) |
83 | | simpllr 500 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧
𝑛
<N 𝑘) → 𝑛 ∈ N) |
84 | 68, 83 | ffvelrnd 5324 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧
𝑛
<N 𝑘) → (𝐺‘𝑛) ∈ R) |
85 | | addresr 7005 |
. . . . . . . . 9
⊢ (((𝐺‘𝑛) ∈ R ∧
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ∈ R) → (〈(𝐺‘𝑛), 0R〉 +
〈[〈(〈{𝑙
∣ 𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) =
〈((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ),
0R〉) |
86 | 84, 74, 85 | syl2anc 403 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧
𝑛
<N 𝑘) → (〈(𝐺‘𝑛), 0R〉 +
〈[〈(〈{𝑙
∣ 𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉) =
〈((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ),
0R〉) |
87 | 82, 86 | eqtrd 2113 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑛 ∈ 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〉 · 𝑟) = 1)) = 〈((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ),
0R〉) |
88 | 81, 63, 87 | 3brtr3d 3814 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧
𝑛
<N 𝑘) → 〈(𝐺‘𝑘), 0R〉
<ℝ 〈((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ),
0R〉) |
89 | | ltresr 7007 |
. . . . . 6
⊢
(〈(𝐺‘𝑘), 0R〉
<ℝ 〈((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ), 0R〉 ↔ (𝐺‘𝑘) <R ((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R )) |
90 | 88, 89 | sylib 120 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧
𝑛
<N 𝑘) → (𝐺‘𝑘) <R ((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R )) |
91 | 80, 90 | jca 300 |
. . . 4
⊢ ((((𝜑 ∧ 𝑛 ∈ 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 ))) |
92 | 91 | ex 113 |
. . 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 )))) |
93 | 92 | ralrimiva 2434 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ 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 )))) |
94 | 93 | ralrimiva 2434 |
1
⊢ (𝜑 → ∀𝑛 ∈ 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 )))) |