Step | Hyp | Ref
| Expression |
1 | | simpr 109 |
. . . . 5
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) ∧ 𝑆 <Q
𝑋) → 𝑆 <Q 𝑋) |
2 | | ltrnqi 7383 |
. . . . . 6
⊢ (𝑆 <Q
𝑋 →
(*Q‘𝑋) <Q
(*Q‘𝑆)) |
3 | | simplr 525 |
. . . . . . . . 9
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) ∧ 𝑆 <Q
𝑋) → 𝑋 ∈ Q) |
4 | | recclnq 7354 |
. . . . . . . . 9
⊢ (𝑋 ∈ Q →
(*Q‘𝑋) ∈ Q) |
5 | 3, 4 | syl 14 |
. . . . . . . 8
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) ∧ 𝑆 <Q
𝑋) →
(*Q‘𝑋) ∈ Q) |
6 | | ltrelnq 7327 |
. . . . . . . . . . . 12
⊢
<Q ⊆ (Q ×
Q) |
7 | 6 | brel 4663 |
. . . . . . . . . . 11
⊢ (𝑆 <Q
𝑋 → (𝑆 ∈ Q ∧ 𝑋 ∈
Q)) |
8 | 7 | adantl 275 |
. . . . . . . . . 10
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) ∧ 𝑆 <Q
𝑋) → (𝑆 ∈ Q ∧
𝑋 ∈
Q)) |
9 | 8 | simpld 111 |
. . . . . . . . 9
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) ∧ 𝑆 <Q
𝑋) → 𝑆 ∈ Q) |
10 | | recclnq 7354 |
. . . . . . . . 9
⊢ (𝑆 ∈ Q →
(*Q‘𝑆) ∈ Q) |
11 | 9, 10 | syl 14 |
. . . . . . . 8
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) ∧ 𝑆 <Q
𝑋) →
(*Q‘𝑆) ∈ Q) |
12 | | ltmnqg 7363 |
. . . . . . . 8
⊢
(((*Q‘𝑋) ∈ Q ∧
(*Q‘𝑆) ∈ Q ∧ 𝑋 ∈ Q) →
((*Q‘𝑋) <Q
(*Q‘𝑆) ↔ (𝑋 ·Q
(*Q‘𝑋)) <Q (𝑋
·Q (*Q‘𝑆)))) |
13 | 5, 11, 3, 12 | syl3anc 1233 |
. . . . . . 7
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) ∧ 𝑆 <Q
𝑋) →
((*Q‘𝑋) <Q
(*Q‘𝑆) ↔ (𝑋 ·Q
(*Q‘𝑋)) <Q (𝑋
·Q (*Q‘𝑆)))) |
14 | | ltmnqg 7363 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q
∧ 𝑤 ∈
Q) → (𝑦
<Q 𝑧 ↔ (𝑤 ·Q 𝑦) <Q
(𝑤
·Q 𝑧))) |
15 | 14 | adantl 275 |
. . . . . . . 8
⊢
(((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) ∧ 𝑆 <Q
𝑋) ∧ (𝑦 ∈ Q ∧
𝑧 ∈ Q
∧ 𝑤 ∈
Q)) → (𝑦
<Q 𝑧 ↔ (𝑤 ·Q 𝑦) <Q
(𝑤
·Q 𝑧))) |
16 | | mulclnq 7338 |
. . . . . . . . 9
⊢ ((𝑋 ∈ Q ∧
(*Q‘𝑋) ∈ Q) → (𝑋
·Q (*Q‘𝑋)) ∈
Q) |
17 | 3, 5, 16 | syl2anc 409 |
. . . . . . . 8
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) ∧ 𝑆 <Q
𝑋) → (𝑋
·Q (*Q‘𝑋)) ∈
Q) |
18 | | mulclnq 7338 |
. . . . . . . . 9
⊢ ((𝑋 ∈ Q ∧
(*Q‘𝑆) ∈ Q) → (𝑋
·Q (*Q‘𝑆)) ∈
Q) |
19 | 3, 11, 18 | syl2anc 409 |
. . . . . . . 8
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) ∧ 𝑆 <Q
𝑋) → (𝑋
·Q (*Q‘𝑆)) ∈
Q) |
20 | | elprnqu 7444 |
. . . . . . . . 9
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝑈) → 𝐺 ∈ Q) |
21 | 20 | ad2antrr 485 |
. . . . . . . 8
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) ∧ 𝑆 <Q
𝑋) → 𝐺 ∈ Q) |
22 | | mulcomnqg 7345 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦
·Q 𝑧) = (𝑧 ·Q 𝑦)) |
23 | 22 | adantl 275 |
. . . . . . . 8
⊢
(((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) ∧ 𝑆 <Q
𝑋) ∧ (𝑦 ∈ Q ∧
𝑧 ∈ Q))
→ (𝑦
·Q 𝑧) = (𝑧 ·Q 𝑦)) |
24 | 15, 17, 19, 21, 23 | caovord2d 6022 |
. . . . . . 7
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) ∧ 𝑆 <Q
𝑋) → ((𝑋
·Q (*Q‘𝑋))
<Q (𝑋 ·Q
(*Q‘𝑆)) ↔ ((𝑋 ·Q
(*Q‘𝑋)) ·Q 𝐺) <Q
((𝑋
·Q (*Q‘𝑆))
·Q 𝐺))) |
25 | 13, 24 | bitrd 187 |
. . . . . 6
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) ∧ 𝑆 <Q
𝑋) →
((*Q‘𝑋) <Q
(*Q‘𝑆) ↔ ((𝑋 ·Q
(*Q‘𝑋)) ·Q 𝐺) <Q
((𝑋
·Q (*Q‘𝑆))
·Q 𝐺))) |
26 | 2, 25 | syl5ib 153 |
. . . . 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 7355 |
. . . . . . . 8
⊢ (𝑋 ∈ Q →
(𝑋
·Q (*Q‘𝑋)) =
1Q) |
29 | 28 | oveq1d 5868 |
. . . . . . 7
⊢ (𝑋 ∈ Q →
((𝑋
·Q (*Q‘𝑋))
·Q 𝐺) = (1Q
·Q 𝐺)) |
30 | | 1nq 7328 |
. . . . . . . . 9
⊢
1Q ∈ Q |
31 | | mulcomnqg 7345 |
. . . . . . . . 9
⊢
((1Q ∈ Q ∧ 𝐺 ∈ Q) →
(1Q ·Q 𝐺) = (𝐺 ·Q
1Q)) |
32 | 30, 31 | mpan 422 |
. . . . . . . 8
⊢ (𝐺 ∈ Q →
(1Q ·Q 𝐺) = (𝐺 ·Q
1Q)) |
33 | | mulidnq 7351 |
. . . . . . . 8
⊢ (𝐺 ∈ Q →
(𝐺
·Q 1Q) = 𝐺) |
34 | 32, 33 | eqtrd 2203 |
. . . . . . 7
⊢ (𝐺 ∈ Q →
(1Q ·Q 𝐺) = 𝐺) |
35 | 29, 34 | sylan9eqr 2225 |
. . . . . 6
⊢ ((𝐺 ∈ Q ∧
𝑋 ∈ Q)
→ ((𝑋
·Q (*Q‘𝑋))
·Q 𝐺) = 𝐺) |
36 | 35 | breq1d 3999 |
. . . . 5
⊢ ((𝐺 ∈ Q ∧
𝑋 ∈ Q)
→ (((𝑋
·Q (*Q‘𝑋))
·Q 𝐺) <Q ((𝑋
·Q (*Q‘𝑆))
·Q 𝐺) ↔ 𝐺 <Q ((𝑋
·Q (*Q‘𝑆))
·Q 𝐺))) |
37 | 21, 3, 36 | syl2anc 409 |
. . . 4
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) ∧ 𝑆 <Q
𝑋) → (((𝑋
·Q (*Q‘𝑋))
·Q 𝐺) <Q ((𝑋
·Q (*Q‘𝑆))
·Q 𝐺) ↔ 𝐺 <Q ((𝑋
·Q (*Q‘𝑆))
·Q 𝐺))) |
38 | 27, 37 | mpbid 146 |
. . 3
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) ∧ 𝑆 <Q
𝑋) → 𝐺 <Q ((𝑋
·Q (*Q‘𝑆))
·Q 𝐺)) |
39 | | prcunqu 7447 |
. . . 4
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝑈) → (𝐺 <Q ((𝑋
·Q (*Q‘𝑆))
·Q 𝐺) → ((𝑋 ·Q
(*Q‘𝑆)) ·Q 𝐺) ∈ 𝑈)) |
40 | 39 | ad2antrr 485 |
. . 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 114 |
1
⊢
(((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) → (𝑆 <Q
𝑋 → ((𝑋
·Q (*Q‘𝑆))
·Q 𝐺) ∈ 𝑈)) |