Step | Hyp | Ref
| Expression |
1 | | simpr 103 |
. . . . 5
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) ∧ 𝑋 <Q 𝑆) → 𝑋 <Q 𝑆) |
2 | | ltrnqi 6404 |
. . . . . 6
⊢ (𝑋 <Q
𝑆 →
(*Q‘𝑆) <Q
(*Q‘𝑋)) |
3 | | ltrelnq 6349 |
. . . . . . . . . . . 12
⊢
<Q ⊆ (Q ×
Q) |
4 | 3 | brel 4335 |
. . . . . . . . . . 11
⊢ (𝑋 <Q
𝑆 → (𝑋 ∈
Q ∧ 𝑆 ∈
Q)) |
5 | 4 | adantl 262 |
. . . . . . . . . 10
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) ∧ 𝑋 <Q 𝑆) → (𝑋 ∈
Q ∧ 𝑆 ∈
Q)) |
6 | 5 | simprd 107 |
. . . . . . . . 9
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) ∧ 𝑋 <Q 𝑆) → 𝑆 ∈
Q) |
7 | | recclnq 6376 |
. . . . . . . . 9
⊢ (𝑆 ∈ Q →
(*Q‘𝑆) ∈
Q) |
8 | 6, 7 | syl 14 |
. . . . . . . 8
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) ∧ 𝑋 <Q 𝑆) →
(*Q‘𝑆) ∈
Q) |
9 | | simplr 482 |
. . . . . . . . 9
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) ∧ 𝑋 <Q 𝑆) → 𝑋 ∈
Q) |
10 | | recclnq 6376 |
. . . . . . . . 9
⊢ (𝑋 ∈ Q →
(*Q‘𝑋) ∈
Q) |
11 | 9, 10 | syl 14 |
. . . . . . . 8
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) ∧ 𝑋 <Q 𝑆) →
(*Q‘𝑋) ∈
Q) |
12 | | ltmnqg 6385 |
. . . . . . . 8
⊢
(((*Q‘𝑆) ∈
Q ∧
(*Q‘𝑋) ∈
Q ∧ 𝑋 ∈
Q) → ((*Q‘𝑆) <Q
(*Q‘𝑋) ↔ (𝑋 ·Q
(*Q‘𝑆)) <Q (𝑋
·Q (*Q‘𝑋)))) |
13 | 8, 11, 9, 12 | syl3anc 1134 |
. . . . . . 7
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) ∧ 𝑋 <Q 𝑆) →
((*Q‘𝑆) <Q
(*Q‘𝑋) ↔ (𝑋 ·Q
(*Q‘𝑆)) <Q (𝑋
·Q (*Q‘𝑋)))) |
14 | | ltmnqg 6385 |
. . . . . . . . 9
⊢
((y ∈ Q ∧ z ∈ Q ∧ w ∈ Q) → (y <Q z ↔ (w
·Q y)
<Q (w
·Q z))) |
15 | 14 | adantl 262 |
. . . . . . . 8
⊢
(((((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) ∧ 𝑋 <Q 𝑆) ∧ (y ∈ Q ∧ z ∈ Q ∧ w ∈ Q)) → (y <Q z ↔ (w
·Q y)
<Q (w
·Q z))) |
16 | | mulclnq 6360 |
. . . . . . . . 9
⊢ ((𝑋 ∈ Q ∧ (*Q‘𝑆) ∈ Q) → (𝑋 ·Q
(*Q‘𝑆)) ∈
Q) |
17 | 9, 8, 16 | syl2anc 391 |
. . . . . . . 8
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) ∧ 𝑋 <Q 𝑆) → (𝑋 ·Q
(*Q‘𝑆)) ∈
Q) |
18 | | mulclnq 6360 |
. . . . . . . . 9
⊢ ((𝑋 ∈ Q ∧ (*Q‘𝑋) ∈ Q) → (𝑋 ·Q
(*Q‘𝑋)) ∈
Q) |
19 | 9, 11, 18 | syl2anc 391 |
. . . . . . . 8
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) ∧ 𝑋 <Q 𝑆) → (𝑋 ·Q
(*Q‘𝑋)) ∈
Q) |
20 | | elprnql 6464 |
. . . . . . . . 9
⊢
((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) → 𝐺 ∈
Q) |
21 | 20 | ad2antrr 457 |
. . . . . . . 8
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) ∧ 𝑋 <Q 𝑆) → 𝐺 ∈
Q) |
22 | | mulcomnqg 6367 |
. . . . . . . . 9
⊢
((y ∈ Q ∧ z ∈ Q) → (y ·Q z) = (z
·Q y)) |
23 | 22 | adantl 262 |
. . . . . . . 8
⊢
(((((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) ∧ 𝑋 <Q 𝑆) ∧ (y ∈ Q ∧ z ∈ Q)) → (y ·Q z) = (z
·Q y)) |
24 | 15, 17, 19, 21, 23 | caovord2d 5612 |
. . . . . . 7
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) ∧ 𝑋 <Q 𝑆) → ((𝑋 ·Q
(*Q‘𝑆)) <Q (𝑋
·Q (*Q‘𝑋)) ↔ ((𝑋 ·Q
(*Q‘𝑆)) ·Q 𝐺) <Q
((𝑋
·Q (*Q‘𝑋))
·Q 𝐺))) |
25 | 13, 24 | bitrd 177 |
. . . . . 6
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) ∧ 𝑋 <Q 𝑆) →
((*Q‘𝑆) <Q
(*Q‘𝑋) ↔ ((𝑋 ·Q
(*Q‘𝑆)) ·Q 𝐺) <Q
((𝑋
·Q (*Q‘𝑋))
·Q 𝐺))) |
26 | 2, 25 | syl5ib 143 |
. . . . 5
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) ∧ 𝑋 <Q 𝑆) → (𝑋 <Q 𝑆 → ((𝑋 ·Q
(*Q‘𝑆)) ·Q 𝐺) <Q
((𝑋
·Q (*Q‘𝑋))
·Q 𝐺))) |
27 | 1, 26 | mpd 13 |
. . . 4
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) ∧ 𝑋 <Q 𝑆) → ((𝑋 ·Q
(*Q‘𝑆)) ·Q 𝐺) <Q
((𝑋
·Q (*Q‘𝑋))
·Q 𝐺)) |
28 | | recidnq 6377 |
. . . . . . . 8
⊢ (𝑋 ∈ Q → (𝑋 ·Q
(*Q‘𝑋)) =
1Q) |
29 | 28 | oveq1d 5470 |
. . . . . . 7
⊢ (𝑋 ∈ Q → ((𝑋 ·Q
(*Q‘𝑋)) ·Q 𝐺) = (1Q
·Q 𝐺)) |
30 | | 1nq 6350 |
. . . . . . . . 9
⊢
1Q ∈
Q |
31 | | mulcomnqg 6367 |
. . . . . . . . 9
⊢
((1Q ∈
Q ∧ 𝐺 ∈
Q) → (1Q
·Q 𝐺) = (𝐺 ·Q
1Q)) |
32 | 30, 31 | mpan 400 |
. . . . . . . 8
⊢ (𝐺 ∈ Q →
(1Q ·Q 𝐺) = (𝐺 ·Q
1Q)) |
33 | | mulidnq 6373 |
. . . . . . . 8
⊢ (𝐺 ∈ Q → (𝐺 ·Q
1Q) = 𝐺) |
34 | 32, 33 | eqtrd 2069 |
. . . . . . 7
⊢ (𝐺 ∈ Q →
(1Q ·Q 𝐺) = 𝐺) |
35 | 29, 34 | sylan9eqr 2091 |
. . . . . 6
⊢ ((𝐺 ∈ Q ∧ 𝑋 ∈
Q) → ((𝑋
·Q (*Q‘𝑋))
·Q 𝐺) = 𝐺) |
36 | 35 | breq2d 3767 |
. . . . 5
⊢ ((𝐺 ∈ Q ∧ 𝑋 ∈
Q) → (((𝑋 ·Q
(*Q‘𝑆)) ·Q 𝐺) <Q
((𝑋
·Q (*Q‘𝑋))
·Q 𝐺) ↔ ((𝑋 ·Q
(*Q‘𝑆)) ·Q 𝐺) <Q
𝐺)) |
37 | 21, 9, 36 | syl2anc 391 |
. . . 4
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) ∧ 𝑋 <Q 𝑆) → (((𝑋 ·Q
(*Q‘𝑆)) ·Q 𝐺) <Q
((𝑋
·Q (*Q‘𝑋))
·Q 𝐺) ↔ ((𝑋 ·Q
(*Q‘𝑆)) ·Q 𝐺) <Q
𝐺)) |
38 | 27, 37 | mpbid 135 |
. . 3
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) ∧ 𝑋 <Q 𝑆) → ((𝑋 ·Q
(*Q‘𝑆)) ·Q 𝐺) <Q
𝐺) |
39 | | prcdnql 6467 |
. . . 4
⊢
((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) → (((𝑋 ·Q
(*Q‘𝑆)) ·Q 𝐺) <Q
𝐺 → ((𝑋
·Q (*Q‘𝑆))
·Q 𝐺) ∈ 𝐿)) |
40 | 39 | ad2antrr 457 |
. . 3
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) ∧ 𝑋 <Q 𝑆) → (((𝑋 ·Q
(*Q‘𝑆)) ·Q 𝐺) <Q
𝐺 → ((𝑋
·Q (*Q‘𝑆))
·Q 𝐺) ∈ 𝐿)) |
41 | 38, 40 | mpd 13 |
. 2
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) ∧ 𝑋 <Q 𝑆) → ((𝑋 ·Q
(*Q‘𝑆)) ·Q 𝐺) ∈ 𝐿) |
42 | 41 | ex 108 |
1
⊢
(((〈𝐿, 𝑈〉 ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈
Q) → (𝑋
<Q 𝑆 → ((𝑋 ·Q
(*Q‘𝑆)) ·Q 𝐺) ∈ 𝐿)) |