ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ltmnqg GIF version

Theorem ltmnqg 6881
Description: Ordering property of multiplication for positive fractions. Proposition 9-2.6(iii) of [Gleason] p. 120. (Contributed by Jim Kingdon, 22-Sep-2019.)
Assertion
Ref Expression
ltmnqg ((𝐴Q𝐵Q𝐶Q) → (𝐴 <Q 𝐵 ↔ (𝐶 ·Q 𝐴) <Q (𝐶 ·Q 𝐵)))

Proof of Theorem ltmnqg
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 𝑢 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nqqs 6828 . 2 Q = ((N × N) / ~Q )
2 breq1 3817 . . 3 ([⟨𝑥, 𝑦⟩] ~Q = 𝐴 → ([⟨𝑥, 𝑦⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q𝐴 <Q [⟨𝑧, 𝑤⟩] ~Q ))
3 oveq2 5602 . . . 4 ([⟨𝑥, 𝑦⟩] ~Q = 𝐴 → ([⟨𝑣, 𝑢⟩] ~Q ·Q [⟨𝑥, 𝑦⟩] ~Q ) = ([⟨𝑣, 𝑢⟩] ~Q ·Q 𝐴))
43breq1d 3824 . . 3 ([⟨𝑥, 𝑦⟩] ~Q = 𝐴 → (([⟨𝑣, 𝑢⟩] ~Q ·Q [⟨𝑥, 𝑦⟩] ~Q ) <Q ([⟨𝑣, 𝑢⟩] ~Q ·Q [⟨𝑧, 𝑤⟩] ~Q ) ↔ ([⟨𝑣, 𝑢⟩] ~Q ·Q 𝐴) <Q ([⟨𝑣, 𝑢⟩] ~Q ·Q [⟨𝑧, 𝑤⟩] ~Q )))
52, 4bibi12d 233 . 2 ([⟨𝑥, 𝑦⟩] ~Q = 𝐴 → (([⟨𝑥, 𝑦⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ ([⟨𝑣, 𝑢⟩] ~Q ·Q [⟨𝑥, 𝑦⟩] ~Q ) <Q ([⟨𝑣, 𝑢⟩] ~Q ·Q [⟨𝑧, 𝑤⟩] ~Q )) ↔ (𝐴 <Q [⟨𝑧, 𝑤⟩] ~Q ↔ ([⟨𝑣, 𝑢⟩] ~Q ·Q 𝐴) <Q ([⟨𝑣, 𝑢⟩] ~Q ·Q [⟨𝑧, 𝑤⟩] ~Q ))))
6 breq2 3818 . . 3 ([⟨𝑧, 𝑤⟩] ~Q = 𝐵 → (𝐴 <Q [⟨𝑧, 𝑤⟩] ~Q𝐴 <Q 𝐵))
7 oveq2 5602 . . . 4 ([⟨𝑧, 𝑤⟩] ~Q = 𝐵 → ([⟨𝑣, 𝑢⟩] ~Q ·Q [⟨𝑧, 𝑤⟩] ~Q ) = ([⟨𝑣, 𝑢⟩] ~Q ·Q 𝐵))
87breq2d 3826 . . 3 ([⟨𝑧, 𝑤⟩] ~Q = 𝐵 → (([⟨𝑣, 𝑢⟩] ~Q ·Q 𝐴) <Q ([⟨𝑣, 𝑢⟩] ~Q ·Q [⟨𝑧, 𝑤⟩] ~Q ) ↔ ([⟨𝑣, 𝑢⟩] ~Q ·Q 𝐴) <Q ([⟨𝑣, 𝑢⟩] ~Q ·Q 𝐵)))
96, 8bibi12d 233 . 2 ([⟨𝑧, 𝑤⟩] ~Q = 𝐵 → ((𝐴 <Q [⟨𝑧, 𝑤⟩] ~Q ↔ ([⟨𝑣, 𝑢⟩] ~Q ·Q 𝐴) <Q ([⟨𝑣, 𝑢⟩] ~Q ·Q [⟨𝑧, 𝑤⟩] ~Q )) ↔ (𝐴 <Q 𝐵 ↔ ([⟨𝑣, 𝑢⟩] ~Q ·Q 𝐴) <Q ([⟨𝑣, 𝑢⟩] ~Q ·Q 𝐵))))
10 oveq1 5601 . . . 4 ([⟨𝑣, 𝑢⟩] ~Q = 𝐶 → ([⟨𝑣, 𝑢⟩] ~Q ·Q 𝐴) = (𝐶 ·Q 𝐴))
11 oveq1 5601 . . . 4 ([⟨𝑣, 𝑢⟩] ~Q = 𝐶 → ([⟨𝑣, 𝑢⟩] ~Q ·Q 𝐵) = (𝐶 ·Q 𝐵))
1210, 11breq12d 3827 . . 3 ([⟨𝑣, 𝑢⟩] ~Q = 𝐶 → (([⟨𝑣, 𝑢⟩] ~Q ·Q 𝐴) <Q ([⟨𝑣, 𝑢⟩] ~Q ·Q 𝐵) ↔ (𝐶 ·Q 𝐴) <Q (𝐶 ·Q 𝐵)))
1312bibi2d 230 . 2 ([⟨𝑣, 𝑢⟩] ~Q = 𝐶 → ((𝐴 <Q 𝐵 ↔ ([⟨𝑣, 𝑢⟩] ~Q ·Q 𝐴) <Q ([⟨𝑣, 𝑢⟩] ~Q ·Q 𝐵)) ↔ (𝐴 <Q 𝐵 ↔ (𝐶 ·Q 𝐴) <Q (𝐶 ·Q 𝐵))))
14 mulclpi 6808 . . . . . . . 8 ((𝑓N𝑔N) → (𝑓 ·N 𝑔) ∈ N)
1514adantl 271 . . . . . . 7 ((((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) ∧ (𝑓N𝑔N)) → (𝑓 ·N 𝑔) ∈ N)
16 simp1l 965 . . . . . . 7 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → 𝑥N)
17 simp2r 968 . . . . . . 7 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → 𝑤N)
1815, 16, 17caovcld 5736 . . . . . 6 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (𝑥 ·N 𝑤) ∈ N)
19 simp1r 966 . . . . . . 7 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → 𝑦N)
20 simp2l 967 . . . . . . 7 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → 𝑧N)
2115, 19, 20caovcld 5736 . . . . . 6 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (𝑦 ·N 𝑧) ∈ N)
22 mulclpi 6808 . . . . . . 7 ((𝑣N𝑢N) → (𝑣 ·N 𝑢) ∈ N)
23223ad2ant3 964 . . . . . 6 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (𝑣 ·N 𝑢) ∈ N)
24 ltmpig 6819 . . . . . 6 (((𝑥 ·N 𝑤) ∈ N ∧ (𝑦 ·N 𝑧) ∈ N ∧ (𝑣 ·N 𝑢) ∈ N) → ((𝑥 ·N 𝑤) <N (𝑦 ·N 𝑧) ↔ ((𝑣 ·N 𝑢) ·N (𝑥 ·N 𝑤)) <N ((𝑣 ·N 𝑢) ·N (𝑦 ·N 𝑧))))
2518, 21, 23, 24syl3anc 1172 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ((𝑥 ·N 𝑤) <N (𝑦 ·N 𝑧) ↔ ((𝑣 ·N 𝑢) ·N (𝑥 ·N 𝑤)) <N ((𝑣 ·N 𝑢) ·N (𝑦 ·N 𝑧))))
26 simp3l 969 . . . . . . 7 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → 𝑣N)
27 simp3r 970 . . . . . . 7 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → 𝑢N)
28 mulcompig 6811 . . . . . . . 8 ((𝑓N𝑔N) → (𝑓 ·N 𝑔) = (𝑔 ·N 𝑓))
2928adantl 271 . . . . . . 7 ((((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) ∧ (𝑓N𝑔N)) → (𝑓 ·N 𝑔) = (𝑔 ·N 𝑓))
30 mulasspig 6812 . . . . . . . 8 ((𝑓N𝑔NN) → ((𝑓 ·N 𝑔) ·N ) = (𝑓 ·N (𝑔 ·N )))
3130adantl 271 . . . . . . 7 ((((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) ∧ (𝑓N𝑔NN)) → ((𝑓 ·N 𝑔) ·N ) = (𝑓 ·N (𝑔 ·N )))
3226, 16, 27, 29, 31, 17, 15caov4d 5767 . . . . . 6 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ((𝑣 ·N 𝑥) ·N (𝑢 ·N 𝑤)) = ((𝑣 ·N 𝑢) ·N (𝑥 ·N 𝑤)))
3327, 19, 26, 29, 31, 20, 15caov4d 5767 . . . . . . 7 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ((𝑢 ·N 𝑦) ·N (𝑣 ·N 𝑧)) = ((𝑢 ·N 𝑣) ·N (𝑦 ·N 𝑧)))
34 mulcompig 6811 . . . . . . . . . 10 ((𝑢N𝑣N) → (𝑢 ·N 𝑣) = (𝑣 ·N 𝑢))
3534oveq1d 5609 . . . . . . . . 9 ((𝑢N𝑣N) → ((𝑢 ·N 𝑣) ·N (𝑦 ·N 𝑧)) = ((𝑣 ·N 𝑢) ·N (𝑦 ·N 𝑧)))
3635ancoms 264 . . . . . . . 8 ((𝑣N𝑢N) → ((𝑢 ·N 𝑣) ·N (𝑦 ·N 𝑧)) = ((𝑣 ·N 𝑢) ·N (𝑦 ·N 𝑧)))
37363ad2ant3 964 . . . . . . 7 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ((𝑢 ·N 𝑣) ·N (𝑦 ·N 𝑧)) = ((𝑣 ·N 𝑢) ·N (𝑦 ·N 𝑧)))
3833, 37eqtrd 2117 . . . . . 6 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ((𝑢 ·N 𝑦) ·N (𝑣 ·N 𝑧)) = ((𝑣 ·N 𝑢) ·N (𝑦 ·N 𝑧)))
3932, 38breq12d 3827 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (((𝑣 ·N 𝑥) ·N (𝑢 ·N 𝑤)) <N ((𝑢 ·N 𝑦) ·N (𝑣 ·N 𝑧)) ↔ ((𝑣 ·N 𝑢) ·N (𝑥 ·N 𝑤)) <N ((𝑣 ·N 𝑢) ·N (𝑦 ·N 𝑧))))
4025, 39bitr4d 189 . . . 4 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ((𝑥 ·N 𝑤) <N (𝑦 ·N 𝑧) ↔ ((𝑣 ·N 𝑥) ·N (𝑢 ·N 𝑤)) <N ((𝑢 ·N 𝑦) ·N (𝑣 ·N 𝑧))))
41 ordpipqqs 6854 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N)) → ([⟨𝑥, 𝑦⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ (𝑥 ·N 𝑤) <N (𝑦 ·N 𝑧)))
42413adant3 961 . . . 4 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ([⟨𝑥, 𝑦⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ (𝑥 ·N 𝑤) <N (𝑦 ·N 𝑧)))
4315, 26, 16caovcld 5736 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (𝑣 ·N 𝑥) ∈ N)
4415, 27, 19caovcld 5736 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (𝑢 ·N 𝑦) ∈ N)
4515, 26, 20caovcld 5736 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (𝑣 ·N 𝑧) ∈ N)
4615, 27, 17caovcld 5736 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (𝑢 ·N 𝑤) ∈ N)
47 ordpipqqs 6854 . . . . 5 ((((𝑣 ·N 𝑥) ∈ N ∧ (𝑢 ·N 𝑦) ∈ N) ∧ ((𝑣 ·N 𝑧) ∈ N ∧ (𝑢 ·N 𝑤) ∈ N)) → ([⟨(𝑣 ·N 𝑥), (𝑢 ·N 𝑦)⟩] ~Q <Q [⟨(𝑣 ·N 𝑧), (𝑢 ·N 𝑤)⟩] ~Q ↔ ((𝑣 ·N 𝑥) ·N (𝑢 ·N 𝑤)) <N ((𝑢 ·N 𝑦) ·N (𝑣 ·N 𝑧))))
4843, 44, 45, 46, 47syl22anc 1173 . . . 4 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ([⟨(𝑣 ·N 𝑥), (𝑢 ·N 𝑦)⟩] ~Q <Q [⟨(𝑣 ·N 𝑧), (𝑢 ·N 𝑤)⟩] ~Q ↔ ((𝑣 ·N 𝑥) ·N (𝑢 ·N 𝑤)) <N ((𝑢 ·N 𝑦) ·N (𝑣 ·N 𝑧))))
4940, 42, 483bitr4d 218 . . 3 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ([⟨𝑥, 𝑦⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ [⟨(𝑣 ·N 𝑥), (𝑢 ·N 𝑦)⟩] ~Q <Q [⟨(𝑣 ·N 𝑧), (𝑢 ·N 𝑤)⟩] ~Q ))
50 mulpipqqs 6853 . . . . . 6 (((𝑣N𝑢N) ∧ (𝑥N𝑦N)) → ([⟨𝑣, 𝑢⟩] ~Q ·Q [⟨𝑥, 𝑦⟩] ~Q ) = [⟨(𝑣 ·N 𝑥), (𝑢 ·N 𝑦)⟩] ~Q )
5150ancoms 264 . . . . 5 (((𝑥N𝑦N) ∧ (𝑣N𝑢N)) → ([⟨𝑣, 𝑢⟩] ~Q ·Q [⟨𝑥, 𝑦⟩] ~Q ) = [⟨(𝑣 ·N 𝑥), (𝑢 ·N 𝑦)⟩] ~Q )
52513adant2 960 . . . 4 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ([⟨𝑣, 𝑢⟩] ~Q ·Q [⟨𝑥, 𝑦⟩] ~Q ) = [⟨(𝑣 ·N 𝑥), (𝑢 ·N 𝑦)⟩] ~Q )
53 mulpipqqs 6853 . . . . . 6 (((𝑣N𝑢N) ∧ (𝑧N𝑤N)) → ([⟨𝑣, 𝑢⟩] ~Q ·Q [⟨𝑧, 𝑤⟩] ~Q ) = [⟨(𝑣 ·N 𝑧), (𝑢 ·N 𝑤)⟩] ~Q )
5453ancoms 264 . . . . 5 (((𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ([⟨𝑣, 𝑢⟩] ~Q ·Q [⟨𝑧, 𝑤⟩] ~Q ) = [⟨(𝑣 ·N 𝑧), (𝑢 ·N 𝑤)⟩] ~Q )
55543adant1 959 . . . 4 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ([⟨𝑣, 𝑢⟩] ~Q ·Q [⟨𝑧, 𝑤⟩] ~Q ) = [⟨(𝑣 ·N 𝑧), (𝑢 ·N 𝑤)⟩] ~Q )
5652, 55breq12d 3827 . . 3 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (([⟨𝑣, 𝑢⟩] ~Q ·Q [⟨𝑥, 𝑦⟩] ~Q ) <Q ([⟨𝑣, 𝑢⟩] ~Q ·Q [⟨𝑧, 𝑤⟩] ~Q ) ↔ [⟨(𝑣 ·N 𝑥), (𝑢 ·N 𝑦)⟩] ~Q <Q [⟨(𝑣 ·N 𝑧), (𝑢 ·N 𝑤)⟩] ~Q ))
5749, 56bitr4d 189 . 2 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ([⟨𝑥, 𝑦⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ ([⟨𝑣, 𝑢⟩] ~Q ·Q [⟨𝑥, 𝑦⟩] ~Q ) <Q ([⟨𝑣, 𝑢⟩] ~Q ·Q [⟨𝑧, 𝑤⟩] ~Q )))
581, 5, 9, 13, 573ecoptocl 6314 1 ((𝐴Q𝐵Q𝐶Q) → (𝐴 <Q 𝐵 ↔ (𝐶 ·Q 𝐴) <Q (𝐶 ·Q 𝐵)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  w3a 922   = wceq 1287  wcel 1436  cop 3428   class class class wbr 3814  (class class class)co 5594  [cec 6223  Ncnpi 6752   ·N cmi 6754   <N clti 6755   ~Q ceq 6759  Qcnq 6760   ·Q cmq 6763   <Q cltq 6765
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-coll 3922  ax-sep 3925  ax-nul 3933  ax-pow 3977  ax-pr 4003  ax-un 4227  ax-setind 4319  ax-iinf 4369
This theorem depends on definitions:  df-bi 115  df-dc 779  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-ral 2360  df-rex 2361  df-reu 2362  df-rab 2364  df-v 2616  df-sbc 2829  df-csb 2922  df-dif 2988  df-un 2990  df-in 2992  df-ss 2999  df-nul 3273  df-pw 3411  df-sn 3431  df-pr 3432  df-op 3434  df-uni 3631  df-int 3666  df-iun 3709  df-br 3815  df-opab 3869  df-mpt 3870  df-tr 3905  df-eprel 4083  df-id 4087  df-iord 4160  df-on 4162  df-suc 4165  df-iom 4372  df-xp 4410  df-rel 4411  df-cnv 4412  df-co 4413  df-dm 4414  df-rn 4415  df-res 4416  df-ima 4417  df-iota 4937  df-fun 4974  df-fn 4975  df-f 4976  df-f1 4977  df-fo 4978  df-f1o 4979  df-fv 4980  df-ov 5597  df-oprab 5598  df-mpt2 5599  df-1st 5849  df-2nd 5850  df-recs 6005  df-irdg 6070  df-oadd 6120  df-omul 6121  df-er 6225  df-ec 6227  df-qs 6231  df-ni 6784  df-mi 6786  df-lti 6787  df-mpq 6825  df-enq 6827  df-nqqs 6828  df-mqqs 6830  df-ltnqqs 6833
This theorem is referenced by:  ltmnqi  6883  lt2mulnq  6885  ltaddnq  6887  prarloclemarch  6898  prarloclemarch2  6899  ltrnqg  6900  prarloclemlt  6973  addnqprllem  7007  addnqprulem  7008  appdivnq  7043  mulnqprl  7048  mulnqpru  7049  mullocprlem  7050  mulclpr  7052  distrlem4prl  7064  distrlem4pru  7065  1idprl  7070  1idpru  7071  recexprlem1ssl  7113  recexprlem1ssu  7114
  Copyright terms: Public domain W3C validator