Step | Hyp | Ref
| Expression |
1 | | ltexnqi 7421 |
. . . . 5
⊢ (𝑠 <Q
𝑡 → ∃𝑦 ∈ Q (𝑠 +Q
𝑦) = 𝑡) |
2 | 1 | adantl 277 |
. . . 4
⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧
𝑠
<Q 𝑡) → ∃𝑦 ∈ Q (𝑠 +Q 𝑦) = 𝑡) |
3 | | subhalfnqq 7426 |
. . . . . 6
⊢ (𝑦 ∈ Q →
∃𝑥 ∈
Q (𝑥
+Q 𝑥) <Q 𝑦) |
4 | 3 | ad2antrl 490 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧
𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) → ∃𝑥 ∈ Q (𝑥 +Q 𝑥) <Q
𝑦) |
5 | | archrecnq 7675 |
. . . . . . 7
⊢ (𝑥 ∈ Q →
∃𝑐 ∈
N (*Q‘[⟨𝑐, 1o⟩]
~Q ) <Q 𝑥) |
6 | 5 | ad2antrl 490 |
. . . . . 6
⊢
(((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) → ∃𝑐 ∈ N
(*Q‘[⟨𝑐, 1o⟩]
~Q ) <Q 𝑥) |
7 | | simpllr 534 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) → 𝑠 <Q 𝑡) |
8 | 7 | adantr 276 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[⟨𝑐, 1o⟩]
~Q ) <Q 𝑥)) → 𝑠 <Q 𝑡) |
9 | | simplrl 535 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) → 𝑦 ∈ Q) |
10 | 9 | adantr 276 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[⟨𝑐, 1o⟩]
~Q ) <Q 𝑥)) → 𝑦 ∈ Q) |
11 | | simplrr 536 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) → (𝑠 +Q 𝑦) = 𝑡) |
12 | 11 | adantr 276 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[⟨𝑐, 1o⟩]
~Q ) <Q 𝑥)) → (𝑠 +Q 𝑦) = 𝑡) |
13 | | simplrl 535 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[⟨𝑐, 1o⟩]
~Q ) <Q 𝑥)) → 𝑥 ∈ Q) |
14 | | simplrr 536 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[⟨𝑐, 1o⟩]
~Q ) <Q 𝑥)) → (𝑥 +Q 𝑥) <Q
𝑦) |
15 | | simprl 529 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[⟨𝑐, 1o⟩]
~Q ) <Q 𝑥)) → 𝑐 ∈ N) |
16 | | simprr 531 |
. . . . . . . . 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 7696 |
. . . . . . . 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 535 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧
𝑠
<Q 𝑡) → 𝑠 ∈ Q) |
19 | 18 | ad3antrrr 492 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[⟨𝑐, 1o⟩]
~Q ) <Q 𝑥)) → 𝑠 ∈ Q) |
20 | | nnnq 7434 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ N →
[⟨𝑐,
1o⟩] ~Q ∈
Q) |
21 | 20 | ad2antrl 490 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[⟨𝑐, 1o⟩]
~Q ) <Q 𝑥)) → [⟨𝑐, 1o⟩]
~Q ∈ Q) |
22 | | recclnq 7404 |
. . . . . . . . . . . . 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 7387 |
. . . . . . . . . . . 12
⊢ ((𝑠 ∈ Q ∧
(*Q‘[⟨𝑐, 1o⟩]
~Q ) ∈ Q) → (𝑠 +Q
(*Q‘[⟨𝑐, 1o⟩]
~Q )) ∈ Q) |
25 | 19, 23, 24 | syl2anc 411 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[⟨𝑐, 1o⟩]
~Q ) <Q 𝑥)) → (𝑠 +Q
(*Q‘[⟨𝑐, 1o⟩]
~Q )) ∈ Q) |
26 | | nqprlu 7559 |
. . . . . . . . . . 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 7559 |
. . . . . . . . . . 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 7549 |
. . . . . . . . . 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 411 |
. . . . . . . . 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 536 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧
𝑠
<Q 𝑡) → 𝑡 ∈ Q) |
33 | 32 | ad3antrrr 492 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[⟨𝑐, 1o⟩]
~Q ) <Q 𝑥)) → 𝑡 ∈ Q) |
34 | | nqprlu 7559 |
. . . . . . . . . 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 496 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[⟨𝑐, 1o⟩]
~Q ) <Q 𝑥)) → 𝐹:N⟶P) |
38 | 37, 15 | ffvelcdmd 5665 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) ∧ (𝑐 ∈ N ∧
(*Q‘[⟨𝑐, 1o⟩]
~Q ) <Q 𝑥)) → (𝐹‘𝑐) ∈ P) |
39 | | ltrelnq 7377 |
. . . . . . . . . . . . . 14
⊢
<Q ⊆ (Q ×
Q) |
40 | 39 | brel 4690 |
. . . . . . . . . . . . 13
⊢
((*Q‘[⟨𝑐, 1o⟩]
~Q ) <Q 𝑥 →
((*Q‘[⟨𝑐, 1o⟩]
~Q ) ∈ Q ∧ 𝑥 ∈ Q)) |
41 | 40 | simpld 112 |
. . . . . . . . . . . 12
⊢
((*Q‘[⟨𝑐, 1o⟩]
~Q ) <Q 𝑥 →
(*Q‘[⟨𝑐, 1o⟩]
~Q ) ∈ Q) |
42 | 41 | ad2antll 491 |
. . . . . . . . . . 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 7549 |
. . . . . . . . . 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 411 |
. . . . . . . . 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 7608 |
. . . . . . . . . 10
⊢
<P Or P |
47 | | sowlin 4332 |
. . . . . . . . . 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 424 |
. . . . . . . . 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 1248 |
. . . . . . . 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 276 |
. . . . . . . . . 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 535 |
. . . . . . . . . . 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 110 |
. . . . . . . . . . . 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 7631 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P
∧ ℎ ∈
P) → (𝑓<P 𝑔 ↔ (ℎ +P 𝑓)<P
(ℎ
+P 𝑔))) |
55 | 54 | adantl 277 |
. . . . . . . . . . . . 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 276 |
. . . . . . . . . . . . . . 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 411 |
. . . . . . . . . . . . . 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 276 |
. . . . . . . . . . . . 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 7590 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ (𝑓
+P 𝑔) = (𝑔 +P 𝑓)) |
62 | 61 | adantl 277 |
. . . . . . . . . . . . 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 6057 |
. . . . . . . . . . . 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 167 |
. . . . . . . . . . 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 3790 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 𝑐 → ⟨𝑎, 1o⟩ = ⟨𝑐,
1o⟩) |
66 | 65 | eceq1d 6584 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑐 → [⟨𝑎, 1o⟩]
~Q = [⟨𝑐, 1o⟩]
~Q ) |
67 | 66 | fveq2d 5531 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑐 →
(*Q‘[⟨𝑎, 1o⟩]
~Q ) = (*Q‘[⟨𝑐, 1o⟩]
~Q )) |
68 | 67 | oveq2d 5904 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑐 → (𝑠 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q )) = (𝑠 +Q
(*Q‘[⟨𝑐, 1o⟩]
~Q ))) |
69 | 68 | breq2d 4027 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑐 → (𝑝 <Q (𝑠 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q )) ↔ 𝑝 <Q (𝑠 +Q
(*Q‘[⟨𝑐, 1o⟩]
~Q )))) |
70 | 69 | abbidv 2305 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑐 → {𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q ))} = {𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[⟨𝑐, 1o⟩]
~Q ))}) |
71 | 68 | breq1d 4025 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑐 → ((𝑠 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q )) <Q 𝑞 ↔ (𝑠 +Q
(*Q‘[⟨𝑐, 1o⟩]
~Q )) <Q 𝑞)) |
72 | 71 | abbidv 2305 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑐 → {𝑞 ∣ (𝑠 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q )) <Q 𝑞} = {𝑞 ∣ (𝑠 +Q
(*Q‘[⟨𝑐, 1o⟩]
~Q )) <Q 𝑞}) |
73 | 70, 72 | opeq12d 3798 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑐 → ⟨{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q )) <Q 𝑞}⟩ = ⟨{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[⟨𝑐, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[⟨𝑐, 1o⟩]
~Q )) <Q 𝑞}⟩) |
74 | | fveq2 5527 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑐 → (𝐹‘𝑎) = (𝐹‘𝑐)) |
75 | 73, 74 | breq12d 4028 |
. . . . . . . . . . . 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 2853 |
. . . . . . . . . . 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 411 |
. . . . . . . . . 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 7697 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (1st
‘𝐿) ↔ (𝑠 ∈ Q ∧
∃𝑎 ∈
N ⟨{𝑝
∣ 𝑝
<Q (𝑠 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑎))) |
80 | 51, 77, 79 | sylanbrc 417 |
. . . . . . . . 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 115 |
. . . . . . . 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 276 |
. . . . . . . . . 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 5527 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑐 → (𝐹‘𝑏) = (𝐹‘𝑐)) |
84 | | opeq1 3790 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = 𝑐 → ⟨𝑏, 1o⟩ = ⟨𝑐,
1o⟩) |
85 | 84 | eceq1d 6584 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = 𝑐 → [⟨𝑏, 1o⟩]
~Q = [⟨𝑐, 1o⟩]
~Q ) |
86 | 85 | fveq2d 5531 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 𝑐 →
(*Q‘[⟨𝑏, 1o⟩]
~Q ) = (*Q‘[⟨𝑐, 1o⟩]
~Q )) |
87 | 86 | breq2d 4027 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = 𝑐 → (𝑝 <Q
(*Q‘[⟨𝑏, 1o⟩]
~Q ) ↔ 𝑝 <Q
(*Q‘[⟨𝑐, 1o⟩]
~Q ))) |
88 | 87 | abbidv 2305 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑐 → {𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑏, 1o⟩]
~Q )} = {𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑐, 1o⟩]
~Q )}) |
89 | 86 | breq1d 4025 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = 𝑐 →
((*Q‘[⟨𝑏, 1o⟩]
~Q ) <Q 𝑞 ↔
(*Q‘[⟨𝑐, 1o⟩]
~Q ) <Q 𝑞)) |
90 | 89 | abbidv 2305 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑐 → {𝑞 ∣
(*Q‘[⟨𝑏, 1o⟩]
~Q ) <Q 𝑞} = {𝑞 ∣
(*Q‘[⟨𝑐, 1o⟩]
~Q ) <Q 𝑞}) |
91 | 88, 90 | opeq12d 3798 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑐 → ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑏, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑏, 1o⟩]
~Q ) <Q 𝑞}⟩ = ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑐, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑐, 1o⟩]
~Q ) <Q 𝑞}⟩) |
92 | 83, 91 | oveq12d 5906 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑐 → ((𝐹‘𝑏) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑏, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑏, 1o⟩]
~Q ) <Q 𝑞}⟩) = ((𝐹‘𝑐) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑐, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑐, 1o⟩]
~Q ) <Q 𝑞}⟩)) |
93 | 92 | breq1d 4025 |
. . . . . . . . . . . 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 2853 |
. . . . . . . . . . 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 283 |
. . . . . . . . . 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 7698 |
. . . . . . . . . 10
⊢ (𝑡 ∈ (2nd
‘𝐿) ↔ (𝑡 ∈ Q ∧
∃𝑏 ∈
N ((𝐹‘𝑏) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑏, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑏, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}⟩)) |
97 | 82, 95, 96 | sylanbrc 417 |
. . . . . . . . 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 115 |
. . . . . . . 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 787 |
. . . . . . 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 2609 |
. . . . 5
⊢
(((((𝜑 ∧ (𝑠 ∈ Q ∧
𝑡 ∈ Q))
∧ 𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +Q
𝑥)
<Q 𝑦)) → (𝑠 ∈ (1st ‘𝐿) ∨ 𝑡 ∈ (2nd ‘𝐿))) |
102 | 4, 101 | rexlimddv 2609 |
. . . 4
⊢ ((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧
𝑠
<Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +Q
𝑦) = 𝑡)) → (𝑠 ∈ (1st ‘𝐿) ∨ 𝑡 ∈ (2nd ‘𝐿))) |
103 | 2, 102 | rexlimddv 2609 |
. . 3
⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧
𝑠
<Q 𝑡) → (𝑠 ∈ (1st ‘𝐿) ∨ 𝑡 ∈ (2nd ‘𝐿))) |
104 | 103 | ex 115 |
. 2
⊢ ((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) →
(𝑠
<Q 𝑡 → (𝑠 ∈ (1st ‘𝐿) ∨ 𝑡 ∈ (2nd ‘𝐿)))) |
105 | 104 | ralrimivva 2569 |
1
⊢ (𝜑 → ∀𝑠 ∈ Q ∀𝑡 ∈ Q (𝑠 <Q
𝑡 → (𝑠 ∈ (1st
‘𝐿) ∨ 𝑡 ∈ (2nd
‘𝐿)))) |