Step | Hyp | Ref
| Expression |
1 | | ltexnqi 7371 |
. . . . 5
⊢ (𝑠 <Q
𝑡 → ∃𝑦 ∈ Q (𝑠 +Q
𝑦) = 𝑡) |
2 | 1 | adantl 275 |
. . . 4
⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧
𝑠
<Q 𝑡) → ∃𝑦 ∈ Q (𝑠 +Q 𝑦) = 𝑡) |
3 | | subhalfnqq 7376 |
. . . . . 6
⊢ (𝑦 ∈ Q →
∃𝑥 ∈
Q (𝑥
+Q 𝑥) <Q 𝑦) |
4 | 3 | ad2antrl 487 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧
𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) → ∃𝑥 ∈ Q (𝑥 +Q 𝑥) <Q
𝑦) |
5 | | archrecnq 7625 |
. . . . . . 7
⊢ (𝑥 ∈ Q →
∃𝑐 ∈
N (*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥) |
6 | 5 | ad2antrl 487 |
. . . . . 6
⊢
(((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) → ∃𝑐 ∈ N
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥) |
7 | | simpllr 529 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) → 𝑠 <Q 𝑡) |
8 | 7 | adantr 274 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → 𝑠 <Q 𝑡) |
9 | | simplrl 530 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) → 𝑦 ∈ Q) |
10 | 9 | adantr 274 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → 𝑦 ∈ Q) |
11 | | simplrr 531 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) → (𝑠 +Q 𝑦) = 𝑡) |
12 | 11 | adantr 274 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → (𝑠 +Q 𝑦) = 𝑡) |
13 | | simplrl 530 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → 𝑥 ∈ Q) |
14 | | simplrr 531 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → (𝑥 +Q 𝑥) <Q
𝑦) |
15 | | simprl 526 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → 𝑐 ∈ N) |
16 | | simprr 527 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) →
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥) |
17 | 8, 10, 12, 13, 14, 15, 16 | caucvgprprlemloccalc 7646 |
. . . . . . . 8
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → (〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉) |
18 | | simplrl 530 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧
𝑠
<Q 𝑡) → 𝑠 ∈ Q) |
19 | 18 | ad3antrrr 489 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → 𝑠 ∈ Q) |
20 | | nnnq 7384 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ N →
[〈𝑐,
1o〉] ~Q ∈
Q) |
21 | 20 | ad2antrl 487 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → [〈𝑐, 1o〉]
~Q ∈ Q) |
22 | | recclnq 7354 |
. . . . . . . . . . . . 13
⊢
([〈𝑐,
1o〉] ~Q ∈ Q →
(*Q‘[〈𝑐, 1o〉]
~Q ) ∈ Q) |
23 | 21, 22 | syl 14 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) →
(*Q‘[〈𝑐, 1o〉]
~Q ) ∈ Q) |
24 | | addclnq 7337 |
. . . . . . . . . . . 12
⊢ ((𝑠 ∈ Q ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) ∈ Q) → (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) ∈ Q) |
25 | 19, 23, 24 | syl2anc 409 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) ∈ Q) |
26 | | nqprlu 7509 |
. . . . . . . . . . 11
⊢ ((𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) ∈ Q → 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉 ∈
P) |
27 | 25, 26 | syl 14 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉 ∈
P) |
28 | | nqprlu 7509 |
. . . . . . . . . . 11
⊢
((*Q‘[〈𝑐, 1o〉]
~Q ) ∈ Q → 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉 ∈
P) |
29 | 23, 28 | syl 14 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉 ∈
P) |
30 | | addclpr 7499 |
. . . . . . . . . 10
⊢
((〈{𝑝 ∣
𝑝
<Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉 ∈ P
∧ 〈{𝑝 ∣
𝑝
<Q (*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉 ∈ P) →
(〈{𝑝 ∣ 𝑝 <Q
(𝑠
+Q (*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉) ∈
P) |
31 | 27, 29, 30 | syl2anc 409 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → (〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉) ∈
P) |
32 | | simplrr 531 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧
𝑠
<Q 𝑡) → 𝑡 ∈ Q) |
33 | 32 | ad3antrrr 489 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → 𝑡 ∈ Q) |
34 | | nqprlu 7509 |
. . . . . . . . . 10
⊢ (𝑡 ∈ Q →
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉 ∈
P) |
35 | 33, 34 | syl 14 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → 〈{𝑝 ∣ 𝑝 <Q 𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉 ∈
P) |
36 | | caucvgprpr.f |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:N⟶P) |
37 | 36 | ad5antr 493 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → 𝐹:N⟶P) |
38 | 37, 15 | ffvelrnd 5632 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → (𝐹‘𝑐) ∈ P) |
39 | | ltrelnq 7327 |
. . . . . . . . . . . . . 14
⊢
<Q ⊆ (Q ×
Q) |
40 | 39 | brel 4663 |
. . . . . . . . . . . . 13
⊢
((*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥 →
((*Q‘[〈𝑐, 1o〉]
~Q ) ∈ Q ∧ 𝑥 ∈ Q)) |
41 | 40 | simpld 111 |
. . . . . . . . . . . 12
⊢
((*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥 →
(*Q‘[〈𝑐, 1o〉]
~Q ) ∈ Q) |
42 | 41 | ad2antll 488 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) →
(*Q‘[〈𝑐, 1o〉]
~Q ) ∈ Q) |
43 | 42, 28 | syl 14 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉 ∈
P) |
44 | | addclpr 7499 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑐) ∈ P ∧ 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉 ∈ P) →
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉) ∈
P) |
45 | 38, 43, 44 | syl2anc 409 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → ((𝐹‘𝑐) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉) ∈
P) |
46 | | ltsopr 7558 |
. . . . . . . . . 10
⊢
<P Or P |
47 | | sowlin 4305 |
. . . . . . . . . 10
⊢
((<P Or P ∧ ((〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉) ∈ P ∧
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉 ∈ P
∧ ((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉) ∈ P)) →
((〈{𝑝 ∣ 𝑝 <Q
(𝑠
+Q (*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉 → ((〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉) ∨ ((𝐹‘𝑐) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉))) |
48 | 46, 47 | mpan 422 |
. . . . . . . . 9
⊢
(((〈{𝑝 ∣
𝑝
<Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉) ∈ P ∧
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉 ∈ P
∧ ((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉) ∈ P) →
((〈{𝑝 ∣ 𝑝 <Q
(𝑠
+Q (*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉 → ((〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉) ∨ ((𝐹‘𝑐) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉))) |
49 | 31, 35, 45, 48 | syl3anc 1233 |
. . . . . . . 8
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → ((〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉 → ((〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉) ∨ ((𝐹‘𝑐) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉))) |
50 | 17, 49 | mpd 13 |
. . . . . . 7
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → ((〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉) ∨ ((𝐹‘𝑐) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) |
51 | 19 | adantr 274 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) ∧ (〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)) → 𝑠 ∈ Q) |
52 | | simplrl 530 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) ∧ (〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)) → 𝑐 ∈ N) |
53 | | simpr 109 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) ∧ (〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)) → (〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)) |
54 | | ltaprg 7581 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P
∧ ℎ ∈
P) → (𝑓<P 𝑔 ↔ (ℎ +P 𝑓)<P
(ℎ
+P 𝑔))) |
55 | 54 | adantl 275 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) ∧ (〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)) ∧ (𝑓 ∈ P ∧ 𝑔 ∈ P ∧
ℎ ∈ P))
→ (𝑓<P 𝑔 ↔ (ℎ +P 𝑓)<P
(ℎ
+P 𝑔))) |
56 | 42 | adantr 274 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) ∧ (〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)) →
(*Q‘[〈𝑐, 1o〉]
~Q ) ∈ Q) |
57 | 51, 56, 24 | syl2anc 409 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) ∧ (〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)) → (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) ∈ Q) |
58 | 57, 26 | syl 14 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) ∧ (〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)) → 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉 ∈
P) |
59 | 38 | adantr 274 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) ∧ (〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)) → (𝐹‘𝑐) ∈ P) |
60 | 56, 28 | syl 14 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) ∧ (〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)) → 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉 ∈
P) |
61 | | addcomprg 7540 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ (𝑓
+P 𝑔) = (𝑔 +P 𝑓)) |
62 | 61 | adantl 275 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) ∧ (〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)) ∧ (𝑓 ∈ P ∧ 𝑔 ∈ P)) →
(𝑓
+P 𝑔) = (𝑔 +P 𝑓)) |
63 | 55, 58, 59, 60, 62 | caovord2d 6022 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) ∧ (〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)) → (〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑐) ↔ (〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉))) |
64 | 53, 63 | mpbird 166 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) ∧ (〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)) → 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑐)) |
65 | | opeq1 3765 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 𝑐 → 〈𝑎, 1o〉 = 〈𝑐,
1o〉) |
66 | 65 | eceq1d 6549 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑐 → [〈𝑎, 1o〉]
~Q = [〈𝑐, 1o〉]
~Q ) |
67 | 66 | fveq2d 5500 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑐 →
(*Q‘[〈𝑎, 1o〉]
~Q ) = (*Q‘[〈𝑐, 1o〉]
~Q )) |
68 | 67 | oveq2d 5869 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑐 → (𝑠 +Q
(*Q‘[〈𝑎, 1o〉]
~Q )) = (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))) |
69 | 68 | breq2d 4001 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑐 → (𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑎, 1o〉]
~Q )) ↔ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )))) |
70 | 69 | abbidv 2288 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑐 → {𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑎, 1o〉]
~Q ))} = {𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}) |
71 | 68 | breq1d 3999 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑐 → ((𝑠 +Q
(*Q‘[〈𝑎, 1o〉]
~Q )) <Q 𝑞 ↔ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞)) |
72 | 71 | abbidv 2288 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑐 → {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑎, 1o〉]
~Q )) <Q 𝑞} = {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}) |
73 | 70, 72 | opeq12d 3773 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑐 → 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑎, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑎, 1o〉]
~Q )) <Q 𝑞}〉 = 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉) |
74 | | fveq2 5496 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑐 → (𝐹‘𝑎) = (𝐹‘𝑐)) |
75 | 73, 74 | breq12d 4002 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑐 → (〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑎, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑎, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑎) ↔ 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑐))) |
76 | 75 | rspcev 2834 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ N ∧
〈{𝑝 ∣ 𝑝 <Q
(𝑠
+Q (*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑐)) → ∃𝑎 ∈ N 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑎, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑎, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑎)) |
77 | 52, 64, 76 | syl2anc 409 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) ∧ (〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)) → ∃𝑎 ∈ N 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑎, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑎, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑎)) |
78 | | caucvgprpr.lim |
. . . . . . . . . . 11
⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑟 ∈ N
〈{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[〈𝑟, 1o〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉}〉 |
79 | 78 | caucvgprprlemell 7647 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (1st
‘𝐿) ↔ (𝑠 ∈ Q ∧
∃𝑎 ∈
N 〈{𝑝
∣ 𝑝
<Q (𝑠 +Q
(*Q‘[〈𝑎, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑎, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑎))) |
80 | 51, 77, 79 | sylanbrc 415 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) ∧ (〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)) → 𝑠 ∈ (1st ‘𝐿)) |
81 | 80 | ex 114 |
. . . . . . . 8
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → ((〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉) → 𝑠 ∈ (1st ‘𝐿))) |
82 | 33 | adantr 274 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) ∧ ((𝐹‘𝑐) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉) → 𝑡 ∈
Q) |
83 | | fveq2 5496 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑐 → (𝐹‘𝑏) = (𝐹‘𝑐)) |
84 | | opeq1 3765 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = 𝑐 → 〈𝑏, 1o〉 = 〈𝑐,
1o〉) |
85 | 84 | eceq1d 6549 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = 𝑐 → [〈𝑏, 1o〉]
~Q = [〈𝑐, 1o〉]
~Q ) |
86 | 85 | fveq2d 5500 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 𝑐 →
(*Q‘[〈𝑏, 1o〉]
~Q ) = (*Q‘[〈𝑐, 1o〉]
~Q )) |
87 | 86 | breq2d 4001 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = 𝑐 → (𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q ) ↔ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q ))) |
88 | 87 | abbidv 2288 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑐 → {𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )} = {𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}) |
89 | 86 | breq1d 3999 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = 𝑐 →
((*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞 ↔
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞)) |
90 | 89 | abbidv 2288 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑐 → {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞} = {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}) |
91 | 88, 90 | opeq12d 3773 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑐 → 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉 = 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉) |
92 | 83, 91 | oveq12d 5871 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑐 → ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) = ((𝐹‘𝑐) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)) |
93 | 92 | breq1d 3999 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑐 → (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉 ↔ ((𝐹‘𝑐) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) |
94 | 93 | rspcev 2834 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ N ∧
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉) → ∃𝑏 ∈ N ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉) |
95 | 15, 94 | sylan 281 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) ∧ ((𝐹‘𝑐) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉) → ∃𝑏 ∈ N ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉) |
96 | 78 | caucvgprprlemelu 7648 |
. . . . . . . . . 10
⊢ (𝑡 ∈ (2nd
‘𝐿) ↔ (𝑡 ∈ Q ∧
∃𝑏 ∈
N ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) |
97 | 82, 95, 96 | sylanbrc 415 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) ∧ ((𝐹‘𝑐) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉) → 𝑡 ∈ (2nd
‘𝐿)) |
98 | 97 | ex 114 |
. . . . . . . 8
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → (((𝐹‘𝑐) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉 → 𝑡 ∈ (2nd
‘𝐿))) |
99 | 81, 98 | orim12d 781 |
. . . . . . 7
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → (((〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑐, 1o〉]
~Q )) <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
((𝐹‘𝑐) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉) ∨ ((𝐹‘𝑐) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑐, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉) → (𝑠 ∈ (1st
‘𝐿) ∨ 𝑡 ∈ (2nd
‘𝐿)))) |
100 | 50, 99 | mpd 13 |
. . . . . 6
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[〈𝑐, 1o〉]
~Q ) <Q 𝑥)) → (𝑠 ∈ (1st ‘𝐿) ∨ 𝑡 ∈ (2nd ‘𝐿))) |
101 | 6, 100 | rexlimddv 2592 |
. . . . 5
⊢
(((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) → (𝑠 ∈ (1st ‘𝐿) ∨ 𝑡 ∈ (2nd ‘𝐿))) |
102 | 4, 101 | rexlimddv 2592 |
. . . 4
⊢ ((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧
𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) → (𝑠 ∈ (1st ‘𝐿) ∨ 𝑡 ∈ (2nd ‘𝐿))) |
103 | 2, 102 | rexlimddv 2592 |
. . 3
⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧
𝑠
<Q 𝑡) → (𝑠 ∈ (1st ‘𝐿) ∨ 𝑡 ∈ (2nd ‘𝐿))) |
104 | 103 | ex 114 |
. 2
⊢ ((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) →
(𝑠
<Q 𝑡 → (𝑠 ∈ (1st ‘𝐿) ∨ 𝑡 ∈ (2nd ‘𝐿)))) |
105 | 104 | ralrimivva 2552 |
1
⊢ (𝜑 → ∀𝑠 ∈ Q ∀𝑡 ∈ Q (𝑠 <Q
𝑡 → (𝑠 ∈ (1st
‘𝐿) ∨ 𝑡 ∈ (2nd
‘𝐿)))) |