Proof of Theorem ltrnqg
Step | Hyp | Ref
| Expression |
1 | | recclnq 7341 |
. . . 4
⊢ (𝐴 ∈ Q →
(*Q‘𝐴) ∈ Q) |
2 | | recclnq 7341 |
. . . 4
⊢ (𝐵 ∈ Q →
(*Q‘𝐵) ∈ Q) |
3 | | mulclnq 7325 |
. . . 4
⊢
(((*Q‘𝐴) ∈ Q ∧
(*Q‘𝐵) ∈ Q) →
((*Q‘𝐴) ·Q
(*Q‘𝐵)) ∈ Q) |
4 | 1, 2, 3 | syl2an 287 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ((*Q‘𝐴) ·Q
(*Q‘𝐵)) ∈ Q) |
5 | | ltmnqg 7350 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ ((*Q‘𝐴) ·Q
(*Q‘𝐵)) ∈ Q) → (𝐴 <Q
𝐵 ↔
(((*Q‘𝐴) ·Q
(*Q‘𝐵)) ·Q 𝐴) <Q
(((*Q‘𝐴) ·Q
(*Q‘𝐵)) ·Q 𝐵))) |
6 | 4, 5 | mpd3an3 1333 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
<Q 𝐵 ↔
(((*Q‘𝐴) ·Q
(*Q‘𝐵)) ·Q 𝐴) <Q
(((*Q‘𝐴) ·Q
(*Q‘𝐵)) ·Q 𝐵))) |
7 | | simpl 108 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ 𝐴 ∈
Q) |
8 | | mulcomnqg 7332 |
. . . . . 6
⊢
((((*Q‘𝐴) ·Q
(*Q‘𝐵)) ∈ Q ∧ 𝐴 ∈ Q) →
(((*Q‘𝐴) ·Q
(*Q‘𝐵)) ·Q 𝐴) = (𝐴 ·Q
((*Q‘𝐴) ·Q
(*Q‘𝐵)))) |
9 | 4, 7, 8 | syl2anc 409 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (((*Q‘𝐴) ·Q
(*Q‘𝐵)) ·Q 𝐴) = (𝐴 ·Q
((*Q‘𝐴) ·Q
(*Q‘𝐵)))) |
10 | 1 | adantr 274 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (*Q‘𝐴) ∈ Q) |
11 | 2 | adantl 275 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (*Q‘𝐵) ∈ Q) |
12 | | mulassnqg 7333 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
(*Q‘𝐴) ∈ Q ∧
(*Q‘𝐵) ∈ Q) → ((𝐴
·Q (*Q‘𝐴))
·Q (*Q‘𝐵)) = (𝐴 ·Q
((*Q‘𝐴) ·Q
(*Q‘𝐵)))) |
13 | 7, 10, 11, 12 | syl3anc 1233 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ((𝐴
·Q (*Q‘𝐴))
·Q (*Q‘𝐵)) = (𝐴 ·Q
((*Q‘𝐴) ·Q
(*Q‘𝐵)))) |
14 | | mulclnq 7325 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
(*Q‘𝐴) ∈ Q) → (𝐴
·Q (*Q‘𝐴)) ∈
Q) |
15 | 7, 10, 14 | syl2anc 409 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
·Q (*Q‘𝐴)) ∈
Q) |
16 | | mulcomnqg 7332 |
. . . . . 6
⊢ (((𝐴
·Q (*Q‘𝐴)) ∈ Q ∧
(*Q‘𝐵) ∈ Q) → ((𝐴
·Q (*Q‘𝐴))
·Q (*Q‘𝐵)) =
((*Q‘𝐵) ·Q (𝐴
·Q (*Q‘𝐴)))) |
17 | 15, 11, 16 | syl2anc 409 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ((𝐴
·Q (*Q‘𝐴))
·Q (*Q‘𝐵)) =
((*Q‘𝐵) ·Q (𝐴
·Q (*Q‘𝐴)))) |
18 | 9, 13, 17 | 3eqtr2d 2209 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (((*Q‘𝐴) ·Q
(*Q‘𝐵)) ·Q 𝐴) =
((*Q‘𝐵) ·Q (𝐴
·Q (*Q‘𝐴)))) |
19 | | recidnq 7342 |
. . . . . 6
⊢ (𝐴 ∈ Q →
(𝐴
·Q (*Q‘𝐴)) =
1Q) |
20 | 19 | oveq2d 5866 |
. . . . 5
⊢ (𝐴 ∈ Q →
((*Q‘𝐵) ·Q (𝐴
·Q (*Q‘𝐴))) =
((*Q‘𝐵) ·Q
1Q)) |
21 | | mulidnq 7338 |
. . . . . 6
⊢
((*Q‘𝐵) ∈ Q →
((*Q‘𝐵) ·Q
1Q) = (*Q‘𝐵)) |
22 | 2, 21 | syl 14 |
. . . . 5
⊢ (𝐵 ∈ Q →
((*Q‘𝐵) ·Q
1Q) = (*Q‘𝐵)) |
23 | 20, 22 | sylan9eq 2223 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ((*Q‘𝐵) ·Q (𝐴
·Q (*Q‘𝐴))) =
(*Q‘𝐵)) |
24 | 18, 23 | eqtrd 2203 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (((*Q‘𝐴) ·Q
(*Q‘𝐵)) ·Q 𝐴) =
(*Q‘𝐵)) |
25 | | simpr 109 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ 𝐵 ∈
Q) |
26 | | mulassnqg 7333 |
. . . . 5
⊢
(((*Q‘𝐴) ∈ Q ∧
(*Q‘𝐵) ∈ Q ∧ 𝐵 ∈ Q) →
(((*Q‘𝐴) ·Q
(*Q‘𝐵)) ·Q 𝐵) =
((*Q‘𝐴) ·Q
((*Q‘𝐵) ·Q 𝐵))) |
27 | 10, 11, 25, 26 | syl3anc 1233 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (((*Q‘𝐴) ·Q
(*Q‘𝐵)) ·Q 𝐵) =
((*Q‘𝐴) ·Q
((*Q‘𝐵) ·Q 𝐵))) |
28 | | mulcomnqg 7332 |
. . . . . 6
⊢
(((*Q‘𝐵) ∈ Q ∧ 𝐵 ∈ Q) →
((*Q‘𝐵) ·Q 𝐵) = (𝐵 ·Q
(*Q‘𝐵))) |
29 | 11, 25, 28 | syl2anc 409 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ((*Q‘𝐵) ·Q 𝐵) = (𝐵 ·Q
(*Q‘𝐵))) |
30 | 29 | oveq2d 5866 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ((*Q‘𝐴) ·Q
((*Q‘𝐵) ·Q 𝐵)) =
((*Q‘𝐴) ·Q (𝐵
·Q (*Q‘𝐵)))) |
31 | | recidnq 7342 |
. . . . . 6
⊢ (𝐵 ∈ Q →
(𝐵
·Q (*Q‘𝐵)) =
1Q) |
32 | 31 | oveq2d 5866 |
. . . . 5
⊢ (𝐵 ∈ Q →
((*Q‘𝐴) ·Q (𝐵
·Q (*Q‘𝐵))) =
((*Q‘𝐴) ·Q
1Q)) |
33 | | mulidnq 7338 |
. . . . . 6
⊢
((*Q‘𝐴) ∈ Q →
((*Q‘𝐴) ·Q
1Q) = (*Q‘𝐴)) |
34 | 1, 33 | syl 14 |
. . . . 5
⊢ (𝐴 ∈ Q →
((*Q‘𝐴) ·Q
1Q) = (*Q‘𝐴)) |
35 | 32, 34 | sylan9eqr 2225 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ((*Q‘𝐴) ·Q (𝐵
·Q (*Q‘𝐵))) =
(*Q‘𝐴)) |
36 | 27, 30, 35 | 3eqtrd 2207 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (((*Q‘𝐴) ·Q
(*Q‘𝐵)) ·Q 𝐵) =
(*Q‘𝐴)) |
37 | 24, 36 | breq12d 4000 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ((((*Q‘𝐴) ·Q
(*Q‘𝐵)) ·Q 𝐴) <Q
(((*Q‘𝐴) ·Q
(*Q‘𝐵)) ·Q 𝐵) ↔
(*Q‘𝐵) <Q
(*Q‘𝐴))) |
38 | 6, 37 | bitrd 187 |
1
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
<Q 𝐵 ↔
(*Q‘𝐵) <Q
(*Q‘𝐴))) |