Proof of Theorem appdivnq
Step | Hyp | Ref
| Expression |
1 | | simpl 108 |
. . . 4
⊢ ((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) → 𝐴 <Q
𝐵) |
2 | | ltrelnq 7327 |
. . . . . . . 8
⊢
<Q ⊆ (Q ×
Q) |
3 | 2 | brel 4663 |
. . . . . . 7
⊢ (𝐴 <Q
𝐵 → (𝐴 ∈ Q ∧ 𝐵 ∈
Q)) |
4 | 3 | adantr 274 |
. . . . . 6
⊢ ((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) → (𝐴 ∈ Q ∧
𝐵 ∈
Q)) |
5 | 4 | simpld 111 |
. . . . 5
⊢ ((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) → 𝐴 ∈
Q) |
6 | 4 | simprd 113 |
. . . . 5
⊢ ((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) → 𝐵 ∈
Q) |
7 | | recclnq 7354 |
. . . . . 6
⊢ (𝐶 ∈ Q →
(*Q‘𝐶) ∈ Q) |
8 | 7 | adantl 275 |
. . . . 5
⊢ ((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) →
(*Q‘𝐶) ∈ Q) |
9 | | ltmnqg 7363 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ (*Q‘𝐶) ∈ Q) → (𝐴 <Q
𝐵 ↔
((*Q‘𝐶) ·Q 𝐴) <Q
((*Q‘𝐶) ·Q 𝐵))) |
10 | 5, 6, 8, 9 | syl3anc 1233 |
. . . 4
⊢ ((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) → (𝐴 <Q
𝐵 ↔
((*Q‘𝐶) ·Q 𝐴) <Q
((*Q‘𝐶) ·Q 𝐵))) |
11 | 1, 10 | mpbid 146 |
. . 3
⊢ ((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) →
((*Q‘𝐶) ·Q 𝐴) <Q
((*Q‘𝐶) ·Q 𝐵)) |
12 | | ltbtwnnqq 7377 |
. . 3
⊢
(((*Q‘𝐶) ·Q 𝐴) <Q
((*Q‘𝐶) ·Q 𝐵) ↔ ∃𝑚 ∈ Q
(((*Q‘𝐶) ·Q 𝐴) <Q
𝑚 ∧ 𝑚 <Q
((*Q‘𝐶) ·Q 𝐵))) |
13 | 11, 12 | sylib 121 |
. 2
⊢ ((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) → ∃𝑚 ∈ Q
(((*Q‘𝐶) ·Q 𝐴) <Q
𝑚 ∧ 𝑚 <Q
((*Q‘𝐶) ·Q 𝐵))) |
14 | 8 | adantr 274 |
. . . . . . . . 9
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
(*Q‘𝐶) ∈ Q) |
15 | 5 | adantr 274 |
. . . . . . . . 9
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
𝐴 ∈
Q) |
16 | | mulclnq 7338 |
. . . . . . . . 9
⊢
(((*Q‘𝐶) ∈ Q ∧ 𝐴 ∈ Q) →
((*Q‘𝐶) ·Q 𝐴) ∈
Q) |
17 | 14, 15, 16 | syl2anc 409 |
. . . . . . . 8
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
((*Q‘𝐶) ·Q 𝐴) ∈
Q) |
18 | | simpr 109 |
. . . . . . . 8
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
𝑚 ∈
Q) |
19 | | simplr 525 |
. . . . . . . 8
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
𝐶 ∈
Q) |
20 | | ltmnqg 7363 |
. . . . . . . 8
⊢
((((*Q‘𝐶) ·Q 𝐴) ∈ Q ∧
𝑚 ∈ Q
∧ 𝐶 ∈
Q) → (((*Q‘𝐶) ·Q 𝐴) <Q
𝑚 ↔ (𝐶 ·Q
((*Q‘𝐶) ·Q 𝐴))
<Q (𝐶 ·Q 𝑚))) |
21 | 17, 18, 19, 20 | syl3anc 1233 |
. . . . . . 7
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
(((*Q‘𝐶) ·Q 𝐴) <Q
𝑚 ↔ (𝐶 ·Q
((*Q‘𝐶) ·Q 𝐴))
<Q (𝐶 ·Q 𝑚))) |
22 | | recidnq 7355 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ Q →
(𝐶
·Q (*Q‘𝐶)) =
1Q) |
23 | 22 | oveq1d 5868 |
. . . . . . . . . 10
⊢ (𝐶 ∈ Q →
((𝐶
·Q (*Q‘𝐶))
·Q 𝐴) = (1Q
·Q 𝐴)) |
24 | 23 | ad2antlr 486 |
. . . . . . . . 9
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
((𝐶
·Q (*Q‘𝐶))
·Q 𝐴) = (1Q
·Q 𝐴)) |
25 | | mulassnqg 7346 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ Q ∧
(*Q‘𝐶) ∈ Q ∧ 𝐴 ∈ Q) →
((𝐶
·Q (*Q‘𝐶))
·Q 𝐴) = (𝐶 ·Q
((*Q‘𝐶) ·Q 𝐴))) |
26 | 19, 14, 15, 25 | syl3anc 1233 |
. . . . . . . . 9
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
((𝐶
·Q (*Q‘𝐶))
·Q 𝐴) = (𝐶 ·Q
((*Q‘𝐶) ·Q 𝐴))) |
27 | | 1nq 7328 |
. . . . . . . . . . . 12
⊢
1Q ∈ Q |
28 | | mulcomnqg 7345 |
. . . . . . . . . . . 12
⊢
((1Q ∈ Q ∧ 𝐴 ∈ Q) →
(1Q ·Q 𝐴) = (𝐴 ·Q
1Q)) |
29 | 27, 28 | mpan 422 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Q →
(1Q ·Q 𝐴) = (𝐴 ·Q
1Q)) |
30 | | mulidnq 7351 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Q →
(𝐴
·Q 1Q) = 𝐴) |
31 | 29, 30 | eqtrd 2203 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Q →
(1Q ·Q 𝐴) = 𝐴) |
32 | 15, 31 | syl 14 |
. . . . . . . . 9
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
(1Q ·Q 𝐴) = 𝐴) |
33 | 24, 26, 32 | 3eqtr3d 2211 |
. . . . . . . 8
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
(𝐶
·Q ((*Q‘𝐶)
·Q 𝐴)) = 𝐴) |
34 | 33 | breq1d 3999 |
. . . . . . 7
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
((𝐶
·Q ((*Q‘𝐶)
·Q 𝐴)) <Q (𝐶
·Q 𝑚) ↔ 𝐴 <Q (𝐶
·Q 𝑚))) |
35 | 21, 34 | bitrd 187 |
. . . . . 6
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
(((*Q‘𝐶) ·Q 𝐴) <Q
𝑚 ↔ 𝐴 <Q (𝐶
·Q 𝑚))) |
36 | 6 | adantr 274 |
. . . . . . . . 9
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
𝐵 ∈
Q) |
37 | | mulclnq 7338 |
. . . . . . . . 9
⊢
(((*Q‘𝐶) ∈ Q ∧ 𝐵 ∈ Q) →
((*Q‘𝐶) ·Q 𝐵) ∈
Q) |
38 | 14, 36, 37 | syl2anc 409 |
. . . . . . . 8
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
((*Q‘𝐶) ·Q 𝐵) ∈
Q) |
39 | | ltmnqg 7363 |
. . . . . . . 8
⊢ ((𝑚 ∈ Q ∧
((*Q‘𝐶) ·Q 𝐵) ∈ Q ∧
𝐶 ∈ Q)
→ (𝑚
<Q ((*Q‘𝐶)
·Q 𝐵) ↔ (𝐶 ·Q 𝑚) <Q
(𝐶
·Q ((*Q‘𝐶)
·Q 𝐵)))) |
40 | 18, 38, 19, 39 | syl3anc 1233 |
. . . . . . 7
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
(𝑚
<Q ((*Q‘𝐶)
·Q 𝐵) ↔ (𝐶 ·Q 𝑚) <Q
(𝐶
·Q ((*Q‘𝐶)
·Q 𝐵)))) |
41 | 22 | oveq1d 5868 |
. . . . . . . . . 10
⊢ (𝐶 ∈ Q →
((𝐶
·Q (*Q‘𝐶))
·Q 𝐵) = (1Q
·Q 𝐵)) |
42 | 41 | ad2antlr 486 |
. . . . . . . . 9
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
((𝐶
·Q (*Q‘𝐶))
·Q 𝐵) = (1Q
·Q 𝐵)) |
43 | | mulassnqg 7346 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ Q ∧
(*Q‘𝐶) ∈ Q ∧ 𝐵 ∈ Q) →
((𝐶
·Q (*Q‘𝐶))
·Q 𝐵) = (𝐶 ·Q
((*Q‘𝐶) ·Q 𝐵))) |
44 | 19, 14, 36, 43 | syl3anc 1233 |
. . . . . . . . 9
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
((𝐶
·Q (*Q‘𝐶))
·Q 𝐵) = (𝐶 ·Q
((*Q‘𝐶) ·Q 𝐵))) |
45 | | mulcomnqg 7345 |
. . . . . . . . . . . 12
⊢
((1Q ∈ Q ∧ 𝐵 ∈ Q) →
(1Q ·Q 𝐵) = (𝐵 ·Q
1Q)) |
46 | 27, 45 | mpan 422 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ Q →
(1Q ·Q 𝐵) = (𝐵 ·Q
1Q)) |
47 | | mulidnq 7351 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ Q →
(𝐵
·Q 1Q) = 𝐵) |
48 | 46, 47 | eqtrd 2203 |
. . . . . . . . . 10
⊢ (𝐵 ∈ Q →
(1Q ·Q 𝐵) = 𝐵) |
49 | 36, 48 | syl 14 |
. . . . . . . . 9
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
(1Q ·Q 𝐵) = 𝐵) |
50 | 42, 44, 49 | 3eqtr3d 2211 |
. . . . . . . 8
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
(𝐶
·Q ((*Q‘𝐶)
·Q 𝐵)) = 𝐵) |
51 | 50 | breq2d 4001 |
. . . . . . 7
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
((𝐶
·Q 𝑚) <Q (𝐶
·Q ((*Q‘𝐶)
·Q 𝐵)) ↔ (𝐶 ·Q 𝑚) <Q
𝐵)) |
52 | 40, 51 | bitrd 187 |
. . . . . 6
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
(𝑚
<Q ((*Q‘𝐶)
·Q 𝐵) ↔ (𝐶 ·Q 𝑚) <Q
𝐵)) |
53 | 35, 52 | anbi12d 470 |
. . . . 5
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
((((*Q‘𝐶) ·Q 𝐴) <Q
𝑚 ∧ 𝑚 <Q
((*Q‘𝐶) ·Q 𝐵)) ↔ (𝐴 <Q (𝐶
·Q 𝑚) ∧ (𝐶 ·Q 𝑚) <Q
𝐵))) |
54 | | mulcomnqg 7345 |
. . . . . . . 8
⊢ ((𝐶 ∈ Q ∧
𝑚 ∈ Q)
→ (𝐶
·Q 𝑚) = (𝑚 ·Q 𝐶)) |
55 | 19, 18, 54 | syl2anc 409 |
. . . . . . 7
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
(𝐶
·Q 𝑚) = (𝑚 ·Q 𝐶)) |
56 | 55 | breq2d 4001 |
. . . . . 6
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
(𝐴
<Q (𝐶 ·Q 𝑚) ↔ 𝐴 <Q (𝑚
·Q 𝐶))) |
57 | 55 | breq1d 3999 |
. . . . . 6
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
((𝐶
·Q 𝑚) <Q 𝐵 ↔ (𝑚 ·Q 𝐶) <Q
𝐵)) |
58 | 56, 57 | anbi12d 470 |
. . . . 5
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
((𝐴
<Q (𝐶 ·Q 𝑚) ∧ (𝐶 ·Q 𝑚) <Q
𝐵) ↔ (𝐴 <Q
(𝑚
·Q 𝐶) ∧ (𝑚 ·Q 𝐶) <Q
𝐵))) |
59 | 53, 58 | bitrd 187 |
. . . 4
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
((((*Q‘𝐶) ·Q 𝐴) <Q
𝑚 ∧ 𝑚 <Q
((*Q‘𝐶) ·Q 𝐵)) ↔ (𝐴 <Q (𝑚
·Q 𝐶) ∧ (𝑚 ·Q 𝐶) <Q
𝐵))) |
60 | 59 | biimpd 143 |
. . 3
⊢ (((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) ∧ 𝑚 ∈ Q) →
((((*Q‘𝐶) ·Q 𝐴) <Q
𝑚 ∧ 𝑚 <Q
((*Q‘𝐶) ·Q 𝐵)) → (𝐴 <Q (𝑚
·Q 𝐶) ∧ (𝑚 ·Q 𝐶) <Q
𝐵))) |
61 | 60 | reximdva 2572 |
. 2
⊢ ((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) →
(∃𝑚 ∈
Q (((*Q‘𝐶) ·Q 𝐴) <Q
𝑚 ∧ 𝑚 <Q
((*Q‘𝐶) ·Q 𝐵)) → ∃𝑚 ∈ Q (𝐴 <Q
(𝑚
·Q 𝐶) ∧ (𝑚 ·Q 𝐶) <Q
𝐵))) |
62 | 13, 61 | mpd 13 |
1
⊢ ((𝐴 <Q
𝐵 ∧ 𝐶 ∈ Q) → ∃𝑚 ∈ Q (𝐴 <Q
(𝑚
·Q 𝐶) ∧ (𝑚 ·Q 𝐶) <Q
𝐵)) |