Step | Hyp | Ref
| Expression |
1 | | caucvgsr.f |
. . . 4
⊢ (𝜑 → 𝐹:N⟶R) |
2 | | caucvgsr.cau |
. . . 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 )))) |
3 | | caucvgsrlemgt1.gt1 |
. . . 4
⊢ (𝜑 → ∀𝑚 ∈ N
1R <R (𝐹‘𝑚)) |
4 | | eqid 2081 |
. . . 4
⊢ (𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R )) = (𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R )) |
5 | 1, 2, 3, 4 | caucvgsrlemf 6968 |
. . 3
⊢ (𝜑 → (𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R
)):N⟶P) |
6 | 1, 2, 3, 4 | caucvgsrlemcau 6969 |
. . 3
⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N
𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑛)<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉) ∧ ((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑛) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1𝑜〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1𝑜〉]
~Q ) <Q 𝑢}〉)))) |
7 | 1, 2, 3, 4 | caucvgsrlembound 6970 |
. . 3
⊢ (𝜑 → ∀𝑚 ∈ N
1P<P ((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑚)) |
8 | 5, 6, 7 | caucvgprpr 6902 |
. 2
⊢ (𝜑 → ∃𝑎 ∈ P ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏)))) |
9 | | prsrcl 6960 |
. . . 4
⊢ (𝑎 ∈ P →
[〈(𝑎
+P 1P),
1P〉] ~R ∈
R) |
10 | 9 | ad2antrl 473 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) → [〈(𝑎 +P
1P), 1P〉]
~R ∈ R) |
11 | | srpospr 6959 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ R ∧
0R <R 𝑥) → ∃!𝑐 ∈ P [〈(𝑐 +P
1P), 1P〉]
~R = 𝑥) |
12 | | riotacl 5502 |
. . . . . . . . . 10
⊢
(∃!𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥 → (℩𝑐 ∈ P
[〈(𝑐
+P 1P),
1P〉] ~R = 𝑥) ∈
P) |
13 | 11, 12 | syl 14 |
. . . . . . . . 9
⊢ ((𝑥 ∈ R ∧
0R <R 𝑥) → (℩𝑐 ∈ P [〈(𝑐 +P
1P), 1P〉]
~R = 𝑥) ∈ P) |
14 | 13 | adantll 459 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) → (℩𝑐 ∈ P [〈(𝑐 +P
1P), 1P〉]
~R = 𝑥) ∈ P) |
15 | | simplrr 502 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) → ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏)))) |
16 | 15 | adantr 270 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) → ∀𝑏 ∈ P ∃𝑗 ∈ N
∀𝑘 ∈
N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏)))) |
17 | | oveq2 5540 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (℩𝑐 ∈ P
[〈(𝑐
+P 1P),
1P〉] ~R = 𝑥) → (𝑎 +P 𝑏) = (𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥))) |
18 | 17 | breq2d 3797 |
. . . . . . . . . . . 12
⊢ (𝑏 = (℩𝑐 ∈ P
[〈(𝑐
+P 1P),
1P〉] ~R = 𝑥) → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ↔ ((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)))) |
19 | | oveq2 5540 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (℩𝑐 ∈ P
[〈(𝑐
+P 1P),
1P〉] ~R = 𝑥) → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏) = (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥))) |
20 | 19 | breq2d 3797 |
. . . . . . . . . . . 12
⊢ (𝑏 = (℩𝑐 ∈ P
[〈(𝑐
+P 1P),
1P〉] ~R = 𝑥) → (𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏) ↔ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)))) |
21 | 18, 20 | anbi12d 456 |
. . . . . . . . . . 11
⊢ (𝑏 = (℩𝑐 ∈ P
[〈(𝑐
+P 1P),
1P〉] ~R = 𝑥) → ((((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏)) ↔ (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥))))) |
22 | 21 | imbi2d 228 |
. . . . . . . . . 10
⊢ (𝑏 = (℩𝑐 ∈ P
[〈(𝑐
+P 1P),
1P〉] ~R = 𝑥) → ((𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))) ↔ (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)))))) |
23 | 22 | rexralbidv 2392 |
. . . . . . . . 9
⊢ (𝑏 = (℩𝑐 ∈ P
[〈(𝑐
+P 1P),
1P〉] ~R = 𝑥) → (∃𝑗 ∈ N
∀𝑘 ∈
N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))) ↔ ∃𝑗 ∈ N
∀𝑘 ∈
N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)))))) |
24 | 23 | rspcva 2699 |
. . . . . . . 8
⊢
(((℩𝑐
∈ P [〈(𝑐 +P
1P), 1P〉]
~R = 𝑥) ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏)))) → ∃𝑗 ∈ N
∀𝑘 ∈
N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥))))) |
25 | 14, 16, 24 | syl2anc 403 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) → ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <N
𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥))))) |
26 | | nfv 1461 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗𝜑 |
27 | | nfv 1461 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗 𝑎 ∈
P |
28 | | nfcv 2219 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗P |
29 | | nfre1 2407 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗∃𝑗 ∈ N
∀𝑘 ∈
N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))) |
30 | 28, 29 | nfralya 2404 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗∀𝑏 ∈ P ∃𝑗 ∈ N
∀𝑘 ∈
N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))) |
31 | 27, 30 | nfan 1497 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗(𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏)))) |
32 | 26, 31 | nfan 1497 |
. . . . . . . . . 10
⊢
Ⅎ𝑗(𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) |
33 | | nfv 1461 |
. . . . . . . . . 10
⊢
Ⅎ𝑗 𝑥 ∈
R |
34 | 32, 33 | nfan 1497 |
. . . . . . . . 9
⊢
Ⅎ𝑗((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) |
35 | | nfv 1461 |
. . . . . . . . 9
⊢
Ⅎ𝑗0R
<R 𝑥 |
36 | 34, 35 | nfan 1497 |
. . . . . . . 8
⊢
Ⅎ𝑗(((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) |
37 | | nfv 1461 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘𝜑 |
38 | | nfv 1461 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘 𝑎 ∈
P |
39 | | nfcv 2219 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘P |
40 | | nfcv 2219 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘N |
41 | | nfra1 2397 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))) |
42 | 40, 41 | nfrexya 2405 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘∃𝑗 ∈ N
∀𝑘 ∈
N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))) |
43 | 39, 42 | nfralya 2404 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘∀𝑏 ∈ P ∃𝑗 ∈ N
∀𝑘 ∈
N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))) |
44 | 38, 43 | nfan 1497 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘(𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏)))) |
45 | 37, 44 | nfan 1497 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) |
46 | | nfv 1461 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘 𝑥 ∈
R |
47 | 45, 46 | nfan 1497 |
. . . . . . . . . 10
⊢
Ⅎ𝑘((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) |
48 | | nfv 1461 |
. . . . . . . . . 10
⊢
Ⅎ𝑘0R
<R 𝑥 |
49 | 47, 48 | nfan 1497 |
. . . . . . . . 9
⊢
Ⅎ𝑘(((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) |
50 | 5 | ad4antr 477 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) ∧ 𝑘 ∈ N) → (𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R
)):N⟶P) |
51 | | simpr 108 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) ∧ 𝑘 ∈ N) → 𝑘 ∈
N) |
52 | 50, 51 | ffvelrnd 5324 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) ∧ 𝑘 ∈ N) → ((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) ∈ P) |
53 | | simplrl 501 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) → 𝑎 ∈
P) |
54 | 53 | adantr 270 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) → 𝑎 ∈ P) |
55 | | addclpr 6727 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ P ∧
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥) ∈ P) →
(𝑎
+P (℩𝑐 ∈ P [〈(𝑐 +P
1P), 1P〉]
~R = 𝑥)) ∈ P) |
56 | 54, 14, 55 | syl2anc 403 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) → (𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) ∈
P) |
57 | 56 | adantr 270 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) ∧ 𝑘 ∈ N) → (𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) ∈
P) |
58 | | prsrlt 6963 |
. . . . . . . . . . . . 13
⊢ ((((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) ∈ P ∧ (𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) ∈ P)
→ (((𝑧 ∈
N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) ↔ [〈(((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
1P), 1P〉]
~R <R [〈((𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) +P
1P), 1P〉]
~R )) |
59 | 52, 57, 58 | syl2anc 403 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) ∧ 𝑘 ∈ N) → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) ↔ [〈(((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
1P), 1P〉]
~R <R [〈((𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) +P
1P), 1P〉]
~R )) |
60 | 1, 2, 3, 4 | caucvgsrlemfv 6967 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ N) →
[〈(((𝑧 ∈
N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
1P), 1P〉]
~R = (𝐹‘𝑘)) |
61 | 60 | adantlr 460 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑘 ∈ N) →
[〈(((𝑧 ∈
N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
1P), 1P〉]
~R = (𝐹‘𝑘)) |
62 | 61 | adantlr 460 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 𝑘 ∈ N) →
[〈(((𝑧 ∈
N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
1P), 1P〉]
~R = (𝐹‘𝑘)) |
63 | 62 | adantlr 460 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) ∧ 𝑘 ∈ N) →
[〈(((𝑧 ∈
N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
1P), 1P〉]
~R = (𝐹‘𝑘)) |
64 | | prsradd 6962 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ P ∧
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥) ∈ P) →
[〈((𝑎
+P (℩𝑐 ∈ P [〈(𝑐 +P
1P), 1P〉]
~R = 𝑥)) +P
1P), 1P〉]
~R = ([〈(𝑎 +P
1P), 1P〉]
~R +R
[〈((℩𝑐
∈ P [〈(𝑐 +P
1P), 1P〉]
~R = 𝑥) +P
1P), 1P〉]
~R )) |
65 | 54, 14, 64 | syl2anc 403 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) → [〈((𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) +P
1P), 1P〉]
~R = ([〈(𝑎 +P
1P), 1P〉]
~R +R
[〈((℩𝑐
∈ P [〈(𝑐 +P
1P), 1P〉]
~R = 𝑥) +P
1P), 1P〉]
~R )) |
66 | | prsrriota 6964 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ R ∧
0R <R 𝑥) → [〈((℩𝑐 ∈ P
[〈(𝑐
+P 1P),
1P〉] ~R = 𝑥) +P
1P), 1P〉]
~R = 𝑥) |
67 | 66 | oveq2d 5548 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ R ∧
0R <R 𝑥) → ([〈(𝑎 +P
1P), 1P〉]
~R +R
[〈((℩𝑐
∈ P [〈(𝑐 +P
1P), 1P〉]
~R = 𝑥) +P
1P), 1P〉]
~R ) = ([〈(𝑎 +P
1P), 1P〉]
~R +R 𝑥)) |
68 | 67 | adantll 459 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) → ([〈(𝑎 +P
1P), 1P〉]
~R +R
[〈((℩𝑐
∈ P [〈(𝑐 +P
1P), 1P〉]
~R = 𝑥) +P
1P), 1P〉]
~R ) = ([〈(𝑎 +P
1P), 1P〉]
~R +R 𝑥)) |
69 | 65, 68 | eqtrd 2113 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) → [〈((𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) +P
1P), 1P〉]
~R = ([〈(𝑎 +P
1P), 1P〉]
~R +R 𝑥)) |
70 | 69 | adantr 270 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) ∧ 𝑘 ∈ N) →
[〈((𝑎
+P (℩𝑐 ∈ P [〈(𝑐 +P
1P), 1P〉]
~R = 𝑥)) +P
1P), 1P〉]
~R = ([〈(𝑎 +P
1P), 1P〉]
~R +R 𝑥)) |
71 | 63, 70 | breq12d 3798 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) ∧ 𝑘 ∈ N) →
([〈(((𝑧 ∈
N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
1P), 1P〉]
~R <R [〈((𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) +P
1P), 1P〉]
~R ↔ (𝐹‘𝑘) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥))) |
72 | 59, 71 | bitrd 186 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) ∧ 𝑘 ∈ N) → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) ↔ (𝐹‘𝑘) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥))) |
73 | 54 | adantr 270 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) ∧ 𝑘 ∈ N) → 𝑎 ∈
P) |
74 | 14 | adantr 270 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) ∧ 𝑘 ∈ N) →
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥) ∈
P) |
75 | | addclpr 6727 |
. . . . . . . . . . . . . 14
⊢ ((((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) ∈ P ∧
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥) ∈ P) →
(((𝑧 ∈ N
↦ (℩𝑤
∈ P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) ∈
P) |
76 | 52, 74, 75 | syl2anc 403 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) ∧ 𝑘 ∈ N) → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) ∈
P) |
77 | | prsrlt 6963 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ P ∧
(((𝑧 ∈ N
↦ (℩𝑤
∈ P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) ∈ P)
→ (𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) ↔ [〈(𝑎 +P
1P), 1P〉]
~R <R [〈((((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) +P
1P), 1P〉]
~R )) |
78 | 73, 76, 77 | syl2anc 403 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) ∧ 𝑘 ∈ N) → (𝑎<P
(((𝑧 ∈ N
↦ (℩𝑤
∈ P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) ↔ [〈(𝑎 +P
1P), 1P〉]
~R <R [〈((((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) +P
1P), 1P〉]
~R )) |
79 | | prsradd 6962 |
. . . . . . . . . . . . . 14
⊢ ((((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) ∈ P ∧
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥) ∈ P) →
[〈((((𝑧 ∈
N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) +P
1P), 1P〉]
~R = ([〈(((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
1P), 1P〉]
~R +R
[〈((℩𝑐
∈ P [〈(𝑐 +P
1P), 1P〉]
~R = 𝑥) +P
1P), 1P〉]
~R )) |
80 | 52, 74, 79 | syl2anc 403 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) ∧ 𝑘 ∈ N) →
[〈((((𝑧 ∈
N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) +P
1P), 1P〉]
~R = ([〈(((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
1P), 1P〉]
~R +R
[〈((℩𝑐
∈ P [〈(𝑐 +P
1P), 1P〉]
~R = 𝑥) +P
1P), 1P〉]
~R )) |
81 | 80 | breq2d 3797 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) ∧ 𝑘 ∈ N) →
([〈(𝑎
+P 1P),
1P〉] ~R
<R [〈((((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) +P
1P), 1P〉]
~R ↔ [〈(𝑎 +P
1P), 1P〉]
~R <R ([〈(((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
1P), 1P〉]
~R +R
[〈((℩𝑐
∈ P [〈(𝑐 +P
1P), 1P〉]
~R = 𝑥) +P
1P), 1P〉]
~R ))) |
82 | 66 | adantll 459 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) → [〈((℩𝑐 ∈ P
[〈(𝑐
+P 1P),
1P〉] ~R = 𝑥) +P
1P), 1P〉]
~R = 𝑥) |
83 | 82 | adantr 270 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) ∧ 𝑘 ∈ N) →
[〈((℩𝑐
∈ P [〈(𝑐 +P
1P), 1P〉]
~R = 𝑥) +P
1P), 1P〉]
~R = 𝑥) |
84 | 63, 83 | oveq12d 5550 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) ∧ 𝑘 ∈ N) →
([〈(((𝑧 ∈
N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
1P), 1P〉]
~R +R
[〈((℩𝑐
∈ P [〈(𝑐 +P
1P), 1P〉]
~R = 𝑥) +P
1P), 1P〉]
~R ) = ((𝐹‘𝑘) +R 𝑥)) |
85 | 84 | breq2d 3797 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) ∧ 𝑘 ∈ N) →
([〈(𝑎
+P 1P),
1P〉] ~R
<R ([〈(((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
1P), 1P〉]
~R +R
[〈((℩𝑐
∈ P [〈(𝑐 +P
1P), 1P〉]
~R = 𝑥) +P
1P), 1P〉]
~R ) ↔ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑘) +R 𝑥))) |
86 | 78, 81, 85 | 3bitrd 212 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) ∧ 𝑘 ∈ N) → (𝑎<P
(((𝑧 ∈ N
↦ (℩𝑤
∈ P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) ↔ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑘) +R 𝑥))) |
87 | 72, 86 | anbi12d 456 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) ∧ 𝑘 ∈ N) → ((((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥))) ↔ ((𝐹‘𝑘) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑘) +R 𝑥)))) |
88 | 87 | imbi2d 228 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑎 ∈ P ∧
∀𝑏 ∈
P ∃𝑗
∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) ∧ 𝑘 ∈ N) → ((𝑗 <N
𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)))) ↔ (𝑗 <N 𝑘 → ((𝐹‘𝑘) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑘) +R 𝑥))))) |
89 | 49, 88 | ralbida 2362 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) → (∀𝑘 ∈ N (𝑗 <N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)))) ↔ ∀𝑘 ∈ N (𝑗 <N
𝑘 → ((𝐹‘𝑘) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑘) +R 𝑥))))) |
90 | 36, 89 | rexbid 2367 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) → (∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <N
𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P
(℩𝑐 ∈
P [〈(𝑐
+P 1P),
1P〉] ~R = 𝑥)))) ↔ ∃𝑗 ∈ N
∀𝑘 ∈
N (𝑗
<N 𝑘 → ((𝐹‘𝑘) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑘) +R 𝑥))))) |
91 | 25, 90 | mpbid 145 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) → ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <N
𝑘 → ((𝐹‘𝑘) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑘) +R 𝑥)))) |
92 | | breq2 3789 |
. . . . . . . . 9
⊢ (𝑘 = 𝑖 → (𝑗 <N 𝑘 ↔ 𝑗 <N 𝑖)) |
93 | | fveq2 5198 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖)) |
94 | 93 | breq1d 3795 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ↔ (𝐹‘𝑖) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥))) |
95 | 93 | oveq1d 5547 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) +R 𝑥) = ((𝐹‘𝑖) +R 𝑥)) |
96 | 95 | breq2d 3797 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑖 → ([〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑘) +R 𝑥) ↔ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑖) +R 𝑥))) |
97 | 94, 96 | anbi12d 456 |
. . . . . . . . 9
⊢ (𝑘 = 𝑖 → (((𝐹‘𝑘) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑘) +R 𝑥)) ↔ ((𝐹‘𝑖) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑖) +R 𝑥)))) |
98 | 92, 97 | imbi12d 232 |
. . . . . . . 8
⊢ (𝑘 = 𝑖 → ((𝑗 <N 𝑘 → ((𝐹‘𝑘) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑘) +R 𝑥))) ↔ (𝑗 <N 𝑖 → ((𝐹‘𝑖) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑖) +R 𝑥))))) |
99 | 98 | cbvralv 2577 |
. . . . . . 7
⊢
(∀𝑘 ∈
N (𝑗
<N 𝑘 → ((𝐹‘𝑘) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑘) +R 𝑥))) ↔ ∀𝑖 ∈ N (𝑗 <N
𝑖 → ((𝐹‘𝑖) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑖) +R 𝑥)))) |
100 | 99 | rexbii 2373 |
. . . . . 6
⊢
(∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → ((𝐹‘𝑘) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑘) +R 𝑥))) ↔ ∃𝑗 ∈ N
∀𝑖 ∈
N (𝑗
<N 𝑖 → ((𝐹‘𝑖) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑖) +R 𝑥)))) |
101 | 91, 100 | sylib 120 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) ∧
0R <R 𝑥) → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <N
𝑖 → ((𝐹‘𝑖) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑖) +R 𝑥)))) |
102 | 101 | ex 113 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥 ∈ R) →
(0R <R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <N
𝑖 → ((𝐹‘𝑖) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑖) +R 𝑥))))) |
103 | 102 | ralrimiva 2434 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) → ∀𝑥 ∈ R
(0R <R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <N
𝑖 → ((𝐹‘𝑖) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑖) +R 𝑥))))) |
104 | | oveq1 5539 |
. . . . . . . . . 10
⊢ (𝑦 = [〈(𝑎 +P
1P), 1P〉]
~R → (𝑦 +R 𝑥) = ([〈(𝑎 +P
1P), 1P〉]
~R +R 𝑥)) |
105 | 104 | breq2d 3797 |
. . . . . . . . 9
⊢ (𝑦 = [〈(𝑎 +P
1P), 1P〉]
~R → ((𝐹‘𝑖) <R (𝑦 +R
𝑥) ↔ (𝐹‘𝑖) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥))) |
106 | | breq1 3788 |
. . . . . . . . 9
⊢ (𝑦 = [〈(𝑎 +P
1P), 1P〉]
~R → (𝑦 <R ((𝐹‘𝑖) +R 𝑥) ↔ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑖) +R 𝑥))) |
107 | 105, 106 | anbi12d 456 |
. . . . . . . 8
⊢ (𝑦 = [〈(𝑎 +P
1P), 1P〉]
~R → (((𝐹‘𝑖) <R (𝑦 +R
𝑥) ∧ 𝑦 <R ((𝐹‘𝑖) +R 𝑥)) ↔ ((𝐹‘𝑖) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑖) +R 𝑥)))) |
108 | 107 | imbi2d 228 |
. . . . . . 7
⊢ (𝑦 = [〈(𝑎 +P
1P), 1P〉]
~R → ((𝑗 <N 𝑖 → ((𝐹‘𝑖) <R (𝑦 +R
𝑥) ∧ 𝑦 <R ((𝐹‘𝑖) +R 𝑥))) ↔ (𝑗 <N 𝑖 → ((𝐹‘𝑖) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑖) +R 𝑥))))) |
109 | 108 | rexralbidv 2392 |
. . . . . 6
⊢ (𝑦 = [〈(𝑎 +P
1P), 1P〉]
~R → (∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <N
𝑖 → ((𝐹‘𝑖) <R (𝑦 +R
𝑥) ∧ 𝑦 <R ((𝐹‘𝑖) +R 𝑥))) ↔ ∃𝑗 ∈ N
∀𝑖 ∈
N (𝑗
<N 𝑖 → ((𝐹‘𝑖) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑖) +R 𝑥))))) |
110 | 109 | imbi2d 228 |
. . . . 5
⊢ (𝑦 = [〈(𝑎 +P
1P), 1P〉]
~R → ((0R
<R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <N
𝑖 → ((𝐹‘𝑖) <R (𝑦 +R
𝑥) ∧ 𝑦 <R ((𝐹‘𝑖) +R 𝑥)))) ↔
(0R <R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <N
𝑖 → ((𝐹‘𝑖) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑖) +R 𝑥)))))) |
111 | 110 | ralbidv 2368 |
. . . 4
⊢ (𝑦 = [〈(𝑎 +P
1P), 1P〉]
~R → (∀𝑥 ∈ R
(0R <R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <N
𝑖 → ((𝐹‘𝑖) <R (𝑦 +R
𝑥) ∧ 𝑦 <R ((𝐹‘𝑖) +R 𝑥)))) ↔ ∀𝑥 ∈ R
(0R <R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <N
𝑖 → ((𝐹‘𝑖) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑖) +R 𝑥)))))) |
112 | 111 | rspcev 2701 |
. . 3
⊢
(([〈(𝑎
+P 1P),
1P〉] ~R ∈
R ∧ ∀𝑥 ∈ R
(0R <R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <N
𝑖 → ((𝐹‘𝑖) <R
([〈(𝑎
+P 1P),
1P〉] ~R
+R 𝑥) ∧ [〈(𝑎 +P
1P), 1P〉]
~R <R ((𝐹‘𝑖) +R 𝑥))))) → ∃𝑦 ∈ R
∀𝑥 ∈
R (0R <R
𝑥 → ∃𝑗 ∈ N
∀𝑖 ∈
N (𝑗
<N 𝑖 → ((𝐹‘𝑖) <R (𝑦 +R
𝑥) ∧ 𝑦 <R ((𝐹‘𝑖) +R 𝑥))))) |
113 | 10, 103, 112 | syl2anc 403 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P
∃𝑗 ∈
N ∀𝑘
∈ N (𝑗
<N 𝑘 → (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘)<P (𝑎 +P
𝑏) ∧ 𝑎<P (((𝑧 ∈ N ↦
(℩𝑤 ∈
P (𝐹‘𝑧) = [〈(𝑤 +P
1P), 1P〉]
~R ))‘𝑘) +P 𝑏))))) → ∃𝑦 ∈ R
∀𝑥 ∈
R (0R <R
𝑥 → ∃𝑗 ∈ N
∀𝑖 ∈
N (𝑗
<N 𝑖 → ((𝐹‘𝑖) <R (𝑦 +R
𝑥) ∧ 𝑦 <R ((𝐹‘𝑖) +R 𝑥))))) |
114 | 8, 113 | rexlimddv 2481 |
1
⊢ (𝜑 → ∃𝑦 ∈ R ∀𝑥 ∈ R
(0R <R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <N
𝑖 → ((𝐹‘𝑖) <R (𝑦 +R
𝑥) ∧ 𝑦 <R ((𝐹‘𝑖) +R 𝑥))))) |