Proof of Theorem ltrnqg
Step | Hyp | Ref
| Expression |
1 | | recclnq 6376 |
. . . 4
⊢ (A ∈
Q → (*Q‘A) ∈
Q) |
2 | | recclnq 6376 |
. . . 4
⊢ (B ∈
Q → (*Q‘B) ∈
Q) |
3 | | mulclnq 6360 |
. . . 4
⊢
(((*Q‘A) ∈
Q ∧
(*Q‘B) ∈ Q) →
((*Q‘A)
·Q (*Q‘B)) ∈
Q) |
4 | 1, 2, 3 | syl2an 273 |
. . 3
⊢
((A ∈ Q ∧ B ∈ Q) →
((*Q‘A)
·Q (*Q‘B)) ∈
Q) |
5 | | ltmnqg 6385 |
. . 3
⊢
((A ∈ Q ∧ B ∈ Q ∧ ((*Q‘A) ·Q
(*Q‘B))
∈ Q) → (A <Q B ↔
(((*Q‘A)
·Q (*Q‘B)) ·Q A) <Q
(((*Q‘A)
·Q (*Q‘B)) ·Q B))) |
6 | 4, 5 | mpd3an3 1232 |
. 2
⊢
((A ∈ Q ∧ B ∈ Q) → (A <Q B ↔
(((*Q‘A)
·Q (*Q‘B)) ·Q A) <Q
(((*Q‘A)
·Q (*Q‘B)) ·Q B))) |
7 | | simpl 102 |
. . . . . 6
⊢
((A ∈ Q ∧ B ∈ Q) → A ∈
Q) |
8 | | mulcomnqg 6367 |
. . . . . 6
⊢
((((*Q‘A) ·Q
(*Q‘B))
∈ Q ∧ A ∈ Q) →
(((*Q‘A)
·Q (*Q‘B)) ·Q A) = (A
·Q ((*Q‘A) ·Q
(*Q‘B)))) |
9 | 4, 7, 8 | syl2anc 391 |
. . . . 5
⊢
((A ∈ Q ∧ B ∈ Q) →
(((*Q‘A)
·Q (*Q‘B)) ·Q A) = (A
·Q ((*Q‘A) ·Q
(*Q‘B)))) |
10 | 1 | adantr 261 |
. . . . . 6
⊢
((A ∈ Q ∧ B ∈ Q) →
(*Q‘A) ∈ Q) |
11 | 2 | adantl 262 |
. . . . . 6
⊢
((A ∈ Q ∧ B ∈ Q) →
(*Q‘B) ∈ Q) |
12 | | mulassnqg 6368 |
. . . . . 6
⊢
((A ∈ Q ∧ (*Q‘A) ∈
Q ∧
(*Q‘B) ∈ Q) → ((A ·Q
(*Q‘A))
·Q (*Q‘B)) = (A
·Q ((*Q‘A) ·Q
(*Q‘B)))) |
13 | 7, 10, 11, 12 | syl3anc 1134 |
. . . . 5
⊢
((A ∈ Q ∧ B ∈ Q) → ((A ·Q
(*Q‘A))
·Q (*Q‘B)) = (A
·Q ((*Q‘A) ·Q
(*Q‘B)))) |
14 | | mulclnq 6360 |
. . . . . . 7
⊢
((A ∈ Q ∧ (*Q‘A) ∈
Q) → (A
·Q (*Q‘A)) ∈
Q) |
15 | 7, 10, 14 | syl2anc 391 |
. . . . . 6
⊢
((A ∈ Q ∧ B ∈ Q) → (A ·Q
(*Q‘A))
∈ Q) |
16 | | mulcomnqg 6367 |
. . . . . 6
⊢
(((A
·Q (*Q‘A)) ∈
Q ∧
(*Q‘B) ∈ Q) → ((A ·Q
(*Q‘A))
·Q (*Q‘B)) = ((*Q‘B) ·Q (A ·Q
(*Q‘A)))) |
17 | 15, 11, 16 | syl2anc 391 |
. . . . 5
⊢
((A ∈ Q ∧ B ∈ Q) → ((A ·Q
(*Q‘A))
·Q (*Q‘B)) = ((*Q‘B) ·Q (A ·Q
(*Q‘A)))) |
18 | 9, 13, 17 | 3eqtr2d 2075 |
. . . 4
⊢
((A ∈ Q ∧ B ∈ Q) →
(((*Q‘A)
·Q (*Q‘B)) ·Q A) = ((*Q‘B) ·Q (A ·Q
(*Q‘A)))) |
19 | | recidnq 6377 |
. . . . . 6
⊢ (A ∈
Q → (A
·Q (*Q‘A)) = 1Q) |
20 | 19 | oveq2d 5471 |
. . . . 5
⊢ (A ∈
Q → ((*Q‘B) ·Q (A ·Q
(*Q‘A))) =
((*Q‘B)
·Q
1Q)) |
21 | | mulidnq 6373 |
. . . . . 6
⊢
((*Q‘B) ∈
Q → ((*Q‘B) ·Q
1Q) = (*Q‘B)) |
22 | 2, 21 | syl 14 |
. . . . 5
⊢ (B ∈
Q → ((*Q‘B) ·Q
1Q) = (*Q‘B)) |
23 | 20, 22 | sylan9eq 2089 |
. . . 4
⊢
((A ∈ Q ∧ B ∈ Q) →
((*Q‘B)
·Q (A
·Q (*Q‘A))) = (*Q‘B)) |
24 | 18, 23 | eqtrd 2069 |
. . 3
⊢
((A ∈ Q ∧ B ∈ Q) →
(((*Q‘A)
·Q (*Q‘B)) ·Q A) = (*Q‘B)) |
25 | | simpr 103 |
. . . . 5
⊢
((A ∈ Q ∧ B ∈ Q) → B ∈
Q) |
26 | | mulassnqg 6368 |
. . . . 5
⊢
(((*Q‘A) ∈
Q ∧
(*Q‘B) ∈ Q ∧ B ∈ Q) →
(((*Q‘A)
·Q (*Q‘B)) ·Q B) = ((*Q‘A) ·Q
((*Q‘B)
·Q B))) |
27 | 10, 11, 25, 26 | syl3anc 1134 |
. . . 4
⊢
((A ∈ Q ∧ B ∈ Q) →
(((*Q‘A)
·Q (*Q‘B)) ·Q B) = ((*Q‘A) ·Q
((*Q‘B)
·Q B))) |
28 | | mulcomnqg 6367 |
. . . . . 6
⊢
(((*Q‘B) ∈
Q ∧ B ∈
Q) → ((*Q‘B) ·Q B) = (B
·Q (*Q‘B))) |
29 | 11, 25, 28 | syl2anc 391 |
. . . . 5
⊢
((A ∈ Q ∧ B ∈ Q) →
((*Q‘B)
·Q B) =
(B ·Q
(*Q‘B))) |
30 | 29 | oveq2d 5471 |
. . . 4
⊢
((A ∈ Q ∧ B ∈ Q) →
((*Q‘A)
·Q ((*Q‘B) ·Q B)) = ((*Q‘A) ·Q (B ·Q
(*Q‘B)))) |
31 | | recidnq 6377 |
. . . . . 6
⊢ (B ∈
Q → (B
·Q (*Q‘B)) = 1Q) |
32 | 31 | oveq2d 5471 |
. . . . 5
⊢ (B ∈
Q → ((*Q‘A) ·Q (B ·Q
(*Q‘B))) =
((*Q‘A)
·Q
1Q)) |
33 | | mulidnq 6373 |
. . . . . 6
⊢
((*Q‘A) ∈
Q → ((*Q‘A) ·Q
1Q) = (*Q‘A)) |
34 | 1, 33 | syl 14 |
. . . . 5
⊢ (A ∈
Q → ((*Q‘A) ·Q
1Q) = (*Q‘A)) |
35 | 32, 34 | sylan9eqr 2091 |
. . . 4
⊢
((A ∈ Q ∧ B ∈ Q) →
((*Q‘A)
·Q (B
·Q (*Q‘B))) = (*Q‘A)) |
36 | 27, 30, 35 | 3eqtrd 2073 |
. . 3
⊢
((A ∈ Q ∧ B ∈ Q) →
(((*Q‘A)
·Q (*Q‘B)) ·Q B) = (*Q‘A)) |
37 | 24, 36 | breq12d 3768 |
. 2
⊢
((A ∈ Q ∧ B ∈ Q) →
((((*Q‘A)
·Q (*Q‘B)) ·Q A) <Q
(((*Q‘A)
·Q (*Q‘B)) ·Q B) ↔
(*Q‘B)
<Q (*Q‘A))) |
38 | 6, 37 | bitrd 177 |
1
⊢
((A ∈ Q ∧ B ∈ Q) → (A <Q B ↔ (*Q‘B) <Q
(*Q‘A))) |