Step | Hyp | Ref
| Expression |
1 | | caucvgsr.cau |
. 2
⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N
𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R )))) |
2 | | caucvgsr.f |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:N⟶R) |
3 | | caucvgsrlembnd.bnd |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑚 ∈ N 𝐴 <R (𝐹‘𝑚)) |
4 | | caucvgsrlembnd.offset |
. . . . . . . . . . . 12
⊢ 𝐺 = (𝑎 ∈ N ↦ (((𝐹‘𝑎) +R
1R) +R (𝐴 ·R
-1R))) |
5 | 2, 1, 3, 4 | caucvgsrlemoffval 7716 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ N) → ((𝐺‘𝑛) +R 𝐴) = ((𝐹‘𝑛) +R
1R)) |
6 | 5 | adantr 274 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
((𝐺‘𝑛) +R
𝐴) = ((𝐹‘𝑛) +R
1R)) |
7 | 6 | eqcomd 2163 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
((𝐹‘𝑛) +R
1R) = ((𝐺‘𝑛) +R 𝐴)) |
8 | 2 | ad2antrr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
𝐹:N⟶R) |
9 | | simpr 109 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
𝑘 ∈
N) |
10 | 8, 9 | ffvelrnd 5603 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
(𝐹‘𝑘) ∈ R) |
11 | | simplr 520 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
𝑛 ∈
N) |
12 | | recnnpr 7468 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ N →
〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 ∈
P) |
13 | | prsrcl 7704 |
. . . . . . . . . . . 12
⊢
(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 ∈ P →
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ∈ R) |
14 | 11, 12, 13 | 3syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ∈ R) |
15 | | 1sr 7671 |
. . . . . . . . . . . 12
⊢
1R ∈ R |
16 | 15 | a1i 9 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
1R ∈ R) |
17 | | addcomsrg 7675 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R)
→ (𝑓
+R 𝑔) = (𝑔 +R 𝑓)) |
18 | 17 | adantl 275 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧
(𝑓 ∈ R
∧ 𝑔 ∈
R)) → (𝑓
+R 𝑔) = (𝑔 +R 𝑓)) |
19 | | addasssrg 7676 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R
∧ ℎ ∈
R) → ((𝑓
+R 𝑔) +R ℎ) = (𝑓 +R (𝑔 +R
ℎ))) |
20 | 19 | adantl 275 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧
(𝑓 ∈ R
∧ 𝑔 ∈
R ∧ ℎ
∈ R)) → ((𝑓 +R 𝑔) +R
ℎ) = (𝑓 +R (𝑔 +R
ℎ))) |
21 | 10, 14, 16, 18, 20 | caov32d 6001 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
(((𝐹‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) +R
1R) = (((𝐹‘𝑘) +R
1R) +R [〈(〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R )) |
22 | 2, 1, 3, 4 | caucvgsrlemoffval 7716 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ N) → ((𝐺‘𝑘) +R 𝐴) = ((𝐹‘𝑘) +R
1R)) |
23 | 22 | adantlr 469 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
((𝐺‘𝑘) +R
𝐴) = ((𝐹‘𝑘) +R
1R)) |
24 | 23 | oveq1d 5839 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
(((𝐺‘𝑘) +R
𝐴)
+R [〈(〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) = (((𝐹‘𝑘) +R
1R) +R [〈(〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R )) |
25 | 2, 1, 3, 4 | caucvgsrlemofff 7717 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺:N⟶R) |
26 | 25 | ad2antrr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
𝐺:N⟶R) |
27 | 26, 9 | ffvelrnd 5603 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
(𝐺‘𝑘) ∈ R) |
28 | 3 | caucvgsrlemasr 7710 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ R) |
29 | 28 | ad2antrr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
𝐴 ∈
R) |
30 | 27, 29, 14, 18, 20 | caov32d 6001 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
(((𝐺‘𝑘) +R
𝐴)
+R [〈(〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) = (((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) +R 𝐴)) |
31 | 21, 24, 30 | 3eqtr2d 2196 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
(((𝐹‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) +R
1R) = (((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) +R 𝐴)) |
32 | 7, 31 | breq12d 3978 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
(((𝐹‘𝑛) +R
1R) <R (((𝐹‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) +R
1R) ↔ ((𝐺‘𝑛) +R 𝐴) <R
(((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) +R 𝐴))) |
33 | | ltasrg 7690 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R
∧ ℎ ∈
R) → (𝑓
<R 𝑔 ↔ (ℎ +R 𝑓) <R
(ℎ
+R 𝑔))) |
34 | 33 | adantl 275 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧
(𝑓 ∈ R
∧ 𝑔 ∈
R ∧ ℎ
∈ R)) → (𝑓 <R 𝑔 ↔ (ℎ +R 𝑓) <R
(ℎ
+R 𝑔))) |
35 | 8, 11 | ffvelrnd 5603 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
(𝐹‘𝑛) ∈ R) |
36 | | addclsr 7673 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑘) ∈ R ∧
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ∈ R) → ((𝐹‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ∈ R) |
37 | 10, 14, 36 | syl2anc 409 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
((𝐹‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ∈ R) |
38 | 34, 35, 37, 16, 18 | caovord2d 5990 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
((𝐹‘𝑛) <R
((𝐹‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ↔ ((𝐹‘𝑛) +R
1R) <R (((𝐹‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) +R
1R))) |
39 | 26, 11 | ffvelrnd 5603 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
(𝐺‘𝑛) ∈ R) |
40 | | addclsr 7673 |
. . . . . . . . . 10
⊢ (((𝐺‘𝑘) ∈ R ∧
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ∈ R) → ((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ∈ R) |
41 | 27, 14, 40 | syl2anc 409 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ∈ R) |
42 | 34, 39, 41, 29, 18 | caovord2d 5990 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
((𝐺‘𝑛) <R
((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ↔ ((𝐺‘𝑛) +R 𝐴) <R
(((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) +R 𝐴))) |
43 | 32, 38, 42 | 3bitr4d 219 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
((𝐹‘𝑛) <R
((𝐹‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ↔ (𝐺‘𝑛) <R ((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ))) |
44 | 23 | eqcomd 2163 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
((𝐹‘𝑘) +R
1R) = ((𝐺‘𝑘) +R 𝐴)) |
45 | 35, 14, 16, 18, 20 | caov32d 6001 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
(((𝐹‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) +R
1R) = (((𝐹‘𝑛) +R
1R) +R [〈(〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R )) |
46 | 6 | oveq1d 5839 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
(((𝐺‘𝑛) +R
𝐴)
+R [〈(〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) = (((𝐹‘𝑛) +R
1R) +R [〈(〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R )) |
47 | 39, 29, 14, 18, 20 | caov32d 6001 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
(((𝐺‘𝑛) +R
𝐴)
+R [〈(〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) = (((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) +R 𝐴)) |
48 | 45, 46, 47 | 3eqtr2d 2196 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
(((𝐹‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) +R
1R) = (((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) +R 𝐴)) |
49 | 44, 48 | breq12d 3978 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
(((𝐹‘𝑘) +R
1R) <R (((𝐹‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) +R
1R) ↔ ((𝐺‘𝑘) +R 𝐴) <R
(((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) +R 𝐴))) |
50 | | addclsr 7673 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑛) ∈ R ∧
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ∈ R) → ((𝐹‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ∈ R) |
51 | 35, 14, 50 | syl2anc 409 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
((𝐹‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ∈ R) |
52 | 34, 10, 51, 16, 18 | caovord2d 5990 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
((𝐹‘𝑘) <R
((𝐹‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ↔ ((𝐹‘𝑘) +R
1R) <R (((𝐹‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) +R
1R))) |
53 | | addclsr 7673 |
. . . . . . . . . 10
⊢ (((𝐺‘𝑛) ∈ R ∧
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ∈ R) → ((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ∈ R) |
54 | 39, 14, 53 | syl2anc 409 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ∈ R) |
55 | 34, 27, 54, 29, 18 | caovord2d 5990 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
((𝐺‘𝑘) <R
((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ↔ ((𝐺‘𝑘) +R 𝐴) <R
(((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) +R 𝐴))) |
56 | 49, 52, 55 | 3bitr4d 219 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
((𝐹‘𝑘) <R
((𝐹‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ↔ (𝐺‘𝑘) <R ((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ))) |
57 | 43, 56 | anbi12d 465 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
(((𝐹‘𝑛) <R
((𝐹‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R )) ↔ ((𝐺‘𝑛) <R ((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ∧ (𝐺‘𝑘) <R ((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R )))) |
58 | 57 | biimpd 143 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
(((𝐹‘𝑛) <R
((𝐹‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R )) → ((𝐺‘𝑛) <R ((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ∧ (𝐺‘𝑘) <R ((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R )))) |
59 | 58 | imim2d 54 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) →
((𝑛
<N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ))) → (𝑛 <N 𝑘 → ((𝐺‘𝑛) <R ((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ∧ (𝐺‘𝑘) <R ((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ))))) |
60 | 59 | ralimdva 2524 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ N) →
(∀𝑘 ∈
N (𝑛
<N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ))) → ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐺‘𝑛) <R ((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ∧ (𝐺‘𝑘) <R ((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ))))) |
61 | 60 | ralimdva 2524 |
. 2
⊢ (𝜑 → (∀𝑛 ∈ N
∀𝑘 ∈
N (𝑛
<N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ))) → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N
𝑘 → ((𝐺‘𝑛) <R ((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ∧ (𝐺‘𝑘) <R ((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ))))) |
62 | 1, 61 | mpd 13 |
1
⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N
𝑘 → ((𝐺‘𝑛) <R ((𝐺‘𝑘) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R ) ∧ (𝐺‘𝑘) <R ((𝐺‘𝑛) +R
[〈(〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉 +P
1P), 1P〉]
~R )))) |