Step | Hyp | Ref
| Expression |
1 | | caucvgprprlemloccalc.st |
. . . . . 6
⊢ (𝜑 → 𝑆 <Q 𝑇) |
2 | | ltrelnq 7363 |
. . . . . . 7
⊢
<Q ⊆ (Q ×
Q) |
3 | 2 | brel 4678 |
. . . . . 6
⊢ (𝑆 <Q
𝑇 → (𝑆 ∈ Q ∧ 𝑇 ∈
Q)) |
4 | 1, 3 | syl 14 |
. . . . 5
⊢ (𝜑 → (𝑆 ∈ Q ∧ 𝑇 ∈
Q)) |
5 | 4 | simpld 112 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ Q) |
6 | | caucvgprprlemloccalc.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ N) |
7 | | nnnq 7420 |
. . . . 5
⊢ (𝑀 ∈ N →
[⟨𝑀,
1o⟩] ~Q ∈
Q) |
8 | | recclnq 7390 |
. . . . 5
⊢
([⟨𝑀,
1o⟩] ~Q ∈ Q →
(*Q‘[⟨𝑀, 1o⟩]
~Q ) ∈ Q) |
9 | 6, 7, 8 | 3syl 17 |
. . . 4
⊢ (𝜑 →
(*Q‘[⟨𝑀, 1o⟩]
~Q ) ∈ Q) |
10 | | addclnq 7373 |
. . . 4
⊢ ((𝑆 ∈ Q ∧
(*Q‘[⟨𝑀, 1o⟩]
~Q ) ∈ Q) → (𝑆 +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) ∈ Q) |
11 | 5, 9, 10 | syl2anc 411 |
. . 3
⊢ (𝜑 → (𝑆 +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) ∈ Q) |
12 | | addnqpr 7559 |
. . 3
⊢ (((𝑆 +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) ∈ Q ∧
(*Q‘[⟨𝑀, 1o⟩]
~Q ) ∈ Q) → ⟨{𝑙 ∣ 𝑙 <Q ((𝑆 +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q ))}, {𝑢 ∣ ((𝑆 +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) <Q 𝑢}⟩ = (⟨{𝑙 ∣ 𝑙 <Q (𝑆 +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q ))}, {𝑢 ∣ (𝑆 +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )}, {𝑢 ∣
(*Q‘[⟨𝑀, 1o⟩]
~Q ) <Q 𝑢}⟩)) |
13 | 11, 9, 12 | syl2anc 411 |
. 2
⊢ (𝜑 → ⟨{𝑙 ∣ 𝑙 <Q ((𝑆 +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q ))}, {𝑢 ∣ ((𝑆 +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) <Q 𝑢}⟩ = (⟨{𝑙 ∣ 𝑙 <Q (𝑆 +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q ))}, {𝑢 ∣ (𝑆 +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )}, {𝑢 ∣
(*Q‘[⟨𝑀, 1o⟩]
~Q ) <Q 𝑢}⟩)) |
14 | | addassnqg 7380 |
. . . . 5
⊢ ((𝑆 ∈ Q ∧
(*Q‘[⟨𝑀, 1o⟩]
~Q ) ∈ Q ∧
(*Q‘[⟨𝑀, 1o⟩]
~Q ) ∈ Q) → ((𝑆 +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) = (𝑆 +Q
((*Q‘[⟨𝑀, 1o⟩]
~Q ) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )))) |
15 | 5, 9, 9, 14 | syl3anc 1238 |
. . . 4
⊢ (𝜑 → ((𝑆 +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) = (𝑆 +Q
((*Q‘[⟨𝑀, 1o⟩]
~Q ) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )))) |
16 | | caucvgprprlemloccalc.mx |
. . . . . . . 8
⊢ (𝜑 →
(*Q‘[⟨𝑀, 1o⟩]
~Q ) <Q 𝑋) |
17 | | caucvgprprlemloccalc.x |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ Q) |
18 | | lt2addnq 7402 |
. . . . . . . . 9
⊢
((((*Q‘[⟨𝑀, 1o⟩]
~Q ) ∈ Q ∧ 𝑋 ∈ Q) ∧
((*Q‘[⟨𝑀, 1o⟩]
~Q ) ∈ Q ∧ 𝑋 ∈ Q)) →
(((*Q‘[⟨𝑀, 1o⟩]
~Q ) <Q 𝑋 ∧
(*Q‘[⟨𝑀, 1o⟩]
~Q ) <Q 𝑋) →
((*Q‘[⟨𝑀, 1o⟩]
~Q ) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) <Q (𝑋 +Q
𝑋))) |
19 | 9, 17, 9, 17, 18 | syl22anc 1239 |
. . . . . . . 8
⊢ (𝜑 →
(((*Q‘[⟨𝑀, 1o⟩]
~Q ) <Q 𝑋 ∧
(*Q‘[⟨𝑀, 1o⟩]
~Q ) <Q 𝑋) →
((*Q‘[⟨𝑀, 1o⟩]
~Q ) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) <Q (𝑋 +Q
𝑋))) |
20 | 16, 16, 19 | mp2and 433 |
. . . . . . 7
⊢ (𝜑 →
((*Q‘[⟨𝑀, 1o⟩]
~Q ) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) <Q (𝑋 +Q
𝑋)) |
21 | | caucvgprprlemloccalc.xxy |
. . . . . . 7
⊢ (𝜑 → (𝑋 +Q 𝑋) <Q
𝑌) |
22 | | ltsonq 7396 |
. . . . . . . 8
⊢
<Q Or Q |
23 | 22, 2 | sotri 5024 |
. . . . . . 7
⊢
((((*Q‘[⟨𝑀, 1o⟩]
~Q ) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) <Q (𝑋 +Q
𝑋) ∧ (𝑋 +Q 𝑋) <Q
𝑌) →
((*Q‘[⟨𝑀, 1o⟩]
~Q ) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) <Q 𝑌) |
24 | 20, 21, 23 | syl2anc 411 |
. . . . . 6
⊢ (𝜑 →
((*Q‘[⟨𝑀, 1o⟩]
~Q ) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) <Q 𝑌) |
25 | | ltanqi 7400 |
. . . . . 6
⊢
((((*Q‘[⟨𝑀, 1o⟩]
~Q ) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) <Q 𝑌 ∧ 𝑆 ∈ Q) → (𝑆 +Q
((*Q‘[⟨𝑀, 1o⟩]
~Q ) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q ))) <Q (𝑆 +Q
𝑌)) |
26 | 24, 5, 25 | syl2anc 411 |
. . . . 5
⊢ (𝜑 → (𝑆 +Q
((*Q‘[⟨𝑀, 1o⟩]
~Q ) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q ))) <Q (𝑆 +Q
𝑌)) |
27 | | caucvgprprlemloccalc.syt |
. . . . 5
⊢ (𝜑 → (𝑆 +Q 𝑌) = 𝑇) |
28 | 26, 27 | breqtrd 4029 |
. . . 4
⊢ (𝜑 → (𝑆 +Q
((*Q‘[⟨𝑀, 1o⟩]
~Q ) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q ))) <Q 𝑇) |
29 | 15, 28 | eqbrtrd 4025 |
. . 3
⊢ (𝜑 → ((𝑆 +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) <Q 𝑇) |
30 | | ltnqpri 7592 |
. . 3
⊢ (((𝑆 +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) <Q 𝑇 → ⟨{𝑙 ∣ 𝑙 <Q ((𝑆 +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q ))}, {𝑢 ∣ ((𝑆 +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) <Q 𝑢}⟩<P
⟨{𝑙 ∣ 𝑙 <Q
𝑇}, {𝑢 ∣ 𝑇 <Q 𝑢}⟩) |
31 | 29, 30 | syl 14 |
. 2
⊢ (𝜑 → ⟨{𝑙 ∣ 𝑙 <Q ((𝑆 +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q ))}, {𝑢 ∣ ((𝑆 +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) <Q 𝑢}⟩<P
⟨{𝑙 ∣ 𝑙 <Q
𝑇}, {𝑢 ∣ 𝑇 <Q 𝑢}⟩) |
32 | 13, 31 | eqbrtrrd 4027 |
1
⊢ (𝜑 → (⟨{𝑙 ∣ 𝑙 <Q (𝑆 +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q ))}, {𝑢 ∣ (𝑆 +Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )) <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q
(*Q‘[⟨𝑀, 1o⟩]
~Q )}, {𝑢 ∣
(*Q‘[⟨𝑀, 1o⟩]
~Q ) <Q 𝑢}⟩)<P
⟨{𝑙 ∣ 𝑙 <Q
𝑇}, {𝑢 ∣ 𝑇 <Q 𝑢}⟩) |