Step | Hyp | Ref
| Expression |
1 | | ltrelpi 7286 |
. . . . 5
⊢
<N ⊆ (N ×
N) |
2 | 1 | brel 4663 |
. . . 4
⊢ (𝐴 <N
𝐵 → (𝐴 ∈ N ∧ 𝐵 ∈
N)) |
3 | 2 | adantl 275 |
. . 3
⊢ ((𝜑 ∧ 𝐴 <N 𝐵) → (𝐴 ∈ N ∧ 𝐵 ∈
N)) |
4 | | caucvgprpr.f |
. . . . 5
⊢ (𝜑 → 𝐹:N⟶P) |
5 | | caucvgprpr.cau |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N
𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉)))) |
6 | 4, 5 | caucvgprprlemcbv 7649 |
. . . 4
⊢ (𝜑 → ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑎 <N
𝑏 → ((𝐹‘𝑎)<P ((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑎, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑎, 1o〉]
~Q ) <Q 𝑢}〉) ∧ (𝐹‘𝑏)<P ((𝐹‘𝑎) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑎, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑎, 1o〉]
~Q ) <Q 𝑢}〉)))) |
7 | 6 | adantr 274 |
. . 3
⊢ ((𝜑 ∧ 𝐴 <N 𝐵) → ∀𝑎 ∈ N
∀𝑏 ∈
N (𝑎
<N 𝑏 → ((𝐹‘𝑎)<P ((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑎, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑎, 1o〉]
~Q ) <Q 𝑢}〉) ∧ (𝐹‘𝑏)<P ((𝐹‘𝑎) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑎, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑎, 1o〉]
~Q ) <Q 𝑢}〉)))) |
8 | | simpr 109 |
. . 3
⊢ ((𝜑 ∧ 𝐴 <N 𝐵) → 𝐴 <N 𝐵) |
9 | | breq1 3992 |
. . . . 5
⊢ (𝑎 = 𝐴 → (𝑎 <N 𝑏 ↔ 𝐴 <N 𝑏)) |
10 | | fveq2 5496 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (𝐹‘𝑎) = (𝐹‘𝐴)) |
11 | | opeq1 3765 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝐴 → 〈𝑎, 1o〉 = 〈𝐴,
1o〉) |
12 | 11 | eceq1d 6549 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝐴 → [〈𝑎, 1o〉]
~Q = [〈𝐴, 1o〉]
~Q ) |
13 | 12 | fveq2d 5500 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐴 →
(*Q‘[〈𝑎, 1o〉]
~Q ) = (*Q‘[〈𝐴, 1o〉]
~Q )) |
14 | 13 | breq2d 4001 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → (𝑙 <Q
(*Q‘[〈𝑎, 1o〉]
~Q ) ↔ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q ))) |
15 | 14 | abbidv 2288 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → {𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑎, 1o〉]
~Q )} = {𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}) |
16 | 13 | breq1d 3999 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 →
((*Q‘[〈𝑎, 1o〉]
~Q ) <Q 𝑢 ↔
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢)) |
17 | 16 | abbidv 2288 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → {𝑢 ∣
(*Q‘[〈𝑎, 1o〉]
~Q ) <Q 𝑢} = {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}) |
18 | 15, 17 | opeq12d 3773 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑎, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑎, 1o〉]
~Q ) <Q 𝑢}〉 = 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉) |
19 | 18 | oveq2d 5869 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → ((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑎, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑎, 1o〉]
~Q ) <Q 𝑢}〉) = ((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉)) |
20 | 10, 19 | breq12d 4002 |
. . . . . 6
⊢ (𝑎 = 𝐴 → ((𝐹‘𝑎)<P ((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑎, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑎, 1o〉]
~Q ) <Q 𝑢}〉) ↔ (𝐹‘𝐴)<P ((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉))) |
21 | 10, 18 | oveq12d 5871 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → ((𝐹‘𝑎) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑎, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑎, 1o〉]
~Q ) <Q 𝑢}〉) = ((𝐹‘𝐴) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉)) |
22 | 21 | breq2d 4001 |
. . . . . 6
⊢ (𝑎 = 𝐴 → ((𝐹‘𝑏)<P ((𝐹‘𝑎) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑎, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑎, 1o〉]
~Q ) <Q 𝑢}〉) ↔ (𝐹‘𝑏)<P ((𝐹‘𝐴) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉))) |
23 | 20, 22 | anbi12d 470 |
. . . . 5
⊢ (𝑎 = 𝐴 → (((𝐹‘𝑎)<P ((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑎, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑎, 1o〉]
~Q ) <Q 𝑢}〉) ∧ (𝐹‘𝑏)<P ((𝐹‘𝑎) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑎, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑎, 1o〉]
~Q ) <Q 𝑢}〉)) ↔ ((𝐹‘𝐴)<P ((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉) ∧ (𝐹‘𝑏)<P ((𝐹‘𝐴) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉)))) |
24 | 9, 23 | imbi12d 233 |
. . . 4
⊢ (𝑎 = 𝐴 → ((𝑎 <N 𝑏 → ((𝐹‘𝑎)<P ((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑎, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑎, 1o〉]
~Q ) <Q 𝑢}〉) ∧ (𝐹‘𝑏)<P ((𝐹‘𝑎) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑎, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑎, 1o〉]
~Q ) <Q 𝑢}〉))) ↔ (𝐴 <N 𝑏 → ((𝐹‘𝐴)<P ((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉) ∧ (𝐹‘𝑏)<P ((𝐹‘𝐴) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉))))) |
25 | | breq2 3993 |
. . . . 5
⊢ (𝑏 = 𝐵 → (𝐴 <N 𝑏 ↔ 𝐴 <N 𝐵)) |
26 | | fveq2 5496 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → (𝐹‘𝑏) = (𝐹‘𝐵)) |
27 | 26 | oveq1d 5868 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → ((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉) = ((𝐹‘𝐵) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉)) |
28 | 27 | breq2d 4001 |
. . . . . 6
⊢ (𝑏 = 𝐵 → ((𝐹‘𝐴)<P ((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉) ↔ (𝐹‘𝐴)<P ((𝐹‘𝐵) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉))) |
29 | 26 | breq1d 3999 |
. . . . . 6
⊢ (𝑏 = 𝐵 → ((𝐹‘𝑏)<P ((𝐹‘𝐴) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉) ↔ (𝐹‘𝐵)<P ((𝐹‘𝐴) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉))) |
30 | 28, 29 | anbi12d 470 |
. . . . 5
⊢ (𝑏 = 𝐵 → (((𝐹‘𝐴)<P ((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉) ∧ (𝐹‘𝑏)<P ((𝐹‘𝐴) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉)) ↔ ((𝐹‘𝐴)<P ((𝐹‘𝐵) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉) ∧ (𝐹‘𝐵)<P ((𝐹‘𝐴) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉)))) |
31 | 25, 30 | imbi12d 233 |
. . . 4
⊢ (𝑏 = 𝐵 → ((𝐴 <N 𝑏 → ((𝐹‘𝐴)<P ((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉) ∧ (𝐹‘𝑏)<P ((𝐹‘𝐴) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉))) ↔ (𝐴 <N 𝐵 → ((𝐹‘𝐴)<P ((𝐹‘𝐵) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉) ∧ (𝐹‘𝐵)<P ((𝐹‘𝐴) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉))))) |
32 | 24, 31 | rspc2v 2847 |
. . 3
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ (∀𝑎 ∈
N ∀𝑏
∈ N (𝑎
<N 𝑏 → ((𝐹‘𝑎)<P ((𝐹‘𝑏) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑎, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑎, 1o〉]
~Q ) <Q 𝑢}〉) ∧ (𝐹‘𝑏)<P ((𝐹‘𝑎) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑎, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑎, 1o〉]
~Q ) <Q 𝑢}〉))) → (𝐴 <N 𝐵 → ((𝐹‘𝐴)<P ((𝐹‘𝐵) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉) ∧ (𝐹‘𝐵)<P ((𝐹‘𝐴) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉))))) |
33 | 3, 7, 8, 32 | syl3c 63 |
. 2
⊢ ((𝜑 ∧ 𝐴 <N 𝐵) → ((𝐹‘𝐴)<P ((𝐹‘𝐵) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉) ∧ (𝐹‘𝐵)<P ((𝐹‘𝐴) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉))) |
34 | | breq1 3992 |
. . . . . . 7
⊢ (𝑙 = 𝑝 → (𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q ) ↔ 𝑝 <Q
(*Q‘[〈𝐴, 1o〉]
~Q ))) |
35 | 34 | cbvabv 2295 |
. . . . . 6
⊢ {𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )} = {𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )} |
36 | | breq2 3993 |
. . . . . . 7
⊢ (𝑢 = 𝑞 →
((*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢 ↔
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑞)) |
37 | 36 | cbvabv 2295 |
. . . . . 6
⊢ {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢} = {𝑞 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑞} |
38 | 35, 37 | opeq12i 3770 |
. . . . 5
⊢
〈{𝑙 ∣
𝑙
<Q (*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉 = 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑞}〉 |
39 | 38 | oveq2i 5864 |
. . . 4
⊢ ((𝐹‘𝐵) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉) = ((𝐹‘𝐵) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑞}〉) |
40 | 39 | breq2i 3997 |
. . 3
⊢ ((𝐹‘𝐴)<P ((𝐹‘𝐵) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉) ↔ (𝐹‘𝐴)<P ((𝐹‘𝐵) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑞}〉)) |
41 | 38 | oveq2i 5864 |
. . . 4
⊢ ((𝐹‘𝐴) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉) = ((𝐹‘𝐴) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑞}〉) |
42 | 41 | breq2i 3997 |
. . 3
⊢ ((𝐹‘𝐵)<P ((𝐹‘𝐴) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉) ↔ (𝐹‘𝐵)<P ((𝐹‘𝐴) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑞}〉)) |
43 | 40, 42 | anbi12i 457 |
. 2
⊢ (((𝐹‘𝐴)<P ((𝐹‘𝐵) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉) ∧ (𝐹‘𝐵)<P ((𝐹‘𝐴) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑢}〉)) ↔ ((𝐹‘𝐴)<P ((𝐹‘𝐵) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑞}〉) ∧ (𝐹‘𝐵)<P ((𝐹‘𝐴) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑞}〉))) |
44 | 33, 43 | sylib 121 |
1
⊢ ((𝜑 ∧ 𝐴 <N 𝐵) → ((𝐹‘𝐴)<P ((𝐹‘𝐵) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑞}〉) ∧ (𝐹‘𝐵)<P ((𝐹‘𝐴) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝐴, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝐴, 1o〉]
~Q ) <Q 𝑞}〉))) |