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

Theorem ltmnqg 6385
 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 ((A Q B Q 𝐶 Q) → (A <Q B ↔ (𝐶 ·Q A) <Q (𝐶 ·Q B)))

Proof of Theorem ltmnqg
Dummy variables x y z w v u f g are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nqqs 6332 . 2 Q = ((N × N) / ~Q )
2 breq1 3758 . . 3 ([⟨x, y⟩] ~Q = A → ([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~QA <Q [⟨z, w⟩] ~Q ))
3 oveq2 5463 . . . 4 ([⟨x, y⟩] ~Q = A → ([⟨v, u⟩] ~Q ·Q [⟨x, y⟩] ~Q ) = ([⟨v, u⟩] ~Q ·Q A))
43breq1d 3765 . . 3 ([⟨x, y⟩] ~Q = A → (([⟨v, u⟩] ~Q ·Q [⟨x, y⟩] ~Q ) <Q ([⟨v, u⟩] ~Q ·Q [⟨z, w⟩] ~Q ) ↔ ([⟨v, u⟩] ~Q ·Q A) <Q ([⟨v, u⟩] ~Q ·Q [⟨z, w⟩] ~Q )))
52, 4bibi12d 224 . 2 ([⟨x, y⟩] ~Q = A → (([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ ([⟨v, u⟩] ~Q ·Q [⟨x, y⟩] ~Q ) <Q ([⟨v, u⟩] ~Q ·Q [⟨z, w⟩] ~Q )) ↔ (A <Q [⟨z, w⟩] ~Q ↔ ([⟨v, u⟩] ~Q ·Q A) <Q ([⟨v, u⟩] ~Q ·Q [⟨z, w⟩] ~Q ))))
6 breq2 3759 . . 3 ([⟨z, w⟩] ~Q = B → (A <Q [⟨z, w⟩] ~QA <Q B))
7 oveq2 5463 . . . 4 ([⟨z, w⟩] ~Q = B → ([⟨v, u⟩] ~Q ·Q [⟨z, w⟩] ~Q ) = ([⟨v, u⟩] ~Q ·Q B))
87breq2d 3767 . . 3 ([⟨z, w⟩] ~Q = B → (([⟨v, u⟩] ~Q ·Q A) <Q ([⟨v, u⟩] ~Q ·Q [⟨z, w⟩] ~Q ) ↔ ([⟨v, u⟩] ~Q ·Q A) <Q ([⟨v, u⟩] ~Q ·Q B)))
96, 8bibi12d 224 . 2 ([⟨z, w⟩] ~Q = B → ((A <Q [⟨z, w⟩] ~Q ↔ ([⟨v, u⟩] ~Q ·Q A) <Q ([⟨v, u⟩] ~Q ·Q [⟨z, w⟩] ~Q )) ↔ (A <Q B ↔ ([⟨v, u⟩] ~Q ·Q A) <Q ([⟨v, u⟩] ~Q ·Q B))))
10 oveq1 5462 . . . 4 ([⟨v, u⟩] ~Q = 𝐶 → ([⟨v, u⟩] ~Q ·Q A) = (𝐶 ·Q A))
11 oveq1 5462 . . . 4 ([⟨v, u⟩] ~Q = 𝐶 → ([⟨v, u⟩] ~Q ·Q B) = (𝐶 ·Q B))
1210, 11breq12d 3768 . . 3 ([⟨v, u⟩] ~Q = 𝐶 → (([⟨v, u⟩] ~Q ·Q A) <Q ([⟨v, u⟩] ~Q ·Q B) ↔ (𝐶 ·Q A) <Q (𝐶 ·Q B)))
1312bibi2d 221 . 2 ([⟨v, u⟩] ~Q = 𝐶 → ((A <Q B ↔ ([⟨v, u⟩] ~Q ·Q A) <Q ([⟨v, u⟩] ~Q ·Q B)) ↔ (A <Q B ↔ (𝐶 ·Q A) <Q (𝐶 ·Q B))))
14 mulclpi 6312 . . . . . . . 8 ((f N g N) → (f ·N g) N)
1514adantl 262 . . . . . . 7 ((((x N y N) (z N w N) (v N u N)) (f N g N)) → (f ·N g) N)
16 simp1l 927 . . . . . . 7 (((x N y N) (z N w N) (v N u N)) → x N)
17 simp2r 930 . . . . . . 7 (((x N y N) (z N w N) (v N u N)) → w N)
1815, 16, 17caovcld 5596 . . . . . 6 (((x N y N) (z N w N) (v N u N)) → (x ·N w) N)
19 simp1r 928 . . . . . . 7 (((x N y N) (z N w N) (v N u N)) → y N)
20 simp2l 929 . . . . . . 7 (((x N y N) (z N w N) (v N u N)) → z N)
2115, 19, 20caovcld 5596 . . . . . 6 (((x N y N) (z N w N) (v N u N)) → (y ·N z) N)
22 mulclpi 6312 . . . . . . 7 ((v N u N) → (v ·N u) N)
23223ad2ant3 926 . . . . . 6 (((x N y N) (z N w N) (v N u N)) → (v ·N u) N)
24 ltmpig 6323 . . . . . 6 (((x ·N w) N (y ·N z) N (v ·N u) N) → ((x ·N w) <N (y ·N z) ↔ ((v ·N u) ·N (x ·N w)) <N ((v ·N u) ·N (y ·N z))))
2518, 21, 23, 24syl3anc 1134 . . . . 5 (((x N y N) (z N w N) (v N u N)) → ((x ·N w) <N (y ·N z) ↔ ((v ·N u) ·N (x ·N w)) <N ((v ·N u) ·N (y ·N z))))
26 simp3l 931 . . . . . . 7 (((x N y N) (z N w N) (v N u N)) → v N)
27 simp3r 932 . . . . . . 7 (((x N y N) (z N w N) (v N u N)) → u N)
28 mulcompig 6315 . . . . . . . 8 ((f N g N) → (f ·N g) = (g ·N f))
2928adantl 262 . . . . . . 7 ((((x N y N) (z N w N) (v N u N)) (f N g N)) → (f ·N g) = (g ·N f))
30 mulasspig 6316 . . . . . . . 8 ((f N g N N) → ((f ·N g) ·N ) = (f ·N (g ·N )))
3130adantl 262 . . . . . . 7 ((((x N y N) (z N w N) (v N u N)) (f N g N N)) → ((f ·N g) ·N ) = (f ·N (g ·N )))
3226, 16, 27, 29, 31, 17, 15caov4d 5627 . . . . . 6 (((x N y N) (z N w N) (v N u N)) → ((v ·N x) ·N (u ·N w)) = ((v ·N u) ·N (x ·N w)))
3327, 19, 26, 29, 31, 20, 15caov4d 5627 . . . . . . 7 (((x N y N) (z N w N) (v N u N)) → ((u ·N y) ·N (v ·N z)) = ((u ·N v) ·N (y ·N z)))
34 mulcompig 6315 . . . . . . . . . 10 ((u N v N) → (u ·N v) = (v ·N u))
3534oveq1d 5470 . . . . . . . . 9 ((u N v N) → ((u ·N v) ·N (y ·N z)) = ((v ·N u) ·N (y ·N z)))
3635ancoms 255 . . . . . . . 8 ((v N u N) → ((u ·N v) ·N (y ·N z)) = ((v ·N u) ·N (y ·N z)))
37363ad2ant3 926 . . . . . . 7 (((x N y N) (z N w N) (v N u N)) → ((u ·N v) ·N (y ·N z)) = ((v ·N u) ·N (y ·N z)))
3833, 37eqtrd 2069 . . . . . 6 (((x N y N) (z N w N) (v N u N)) → ((u ·N y) ·N (v ·N z)) = ((v ·N u) ·N (y ·N z)))
3932, 38breq12d 3768 . . . . 5 (((x N y N) (z N w N) (v N u N)) → (((v ·N x) ·N (u ·N w)) <N ((u ·N y) ·N (v ·N z)) ↔ ((v ·N u) ·N (x ·N w)) <N ((v ·N u) ·N (y ·N z))))
4025, 39bitr4d 180 . . . 4 (((x N y N) (z N w N) (v N u N)) → ((x ·N w) <N (y ·N z) ↔ ((v ·N x) ·N (u ·N w)) <N ((u ·N y) ·N (v ·N z))))
41 ordpipqqs 6358 . . . . 5 (((x N y N) (z N w N)) → ([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ (x ·N w) <N (y ·N z)))
42413adant3 923 . . . 4 (((x N y N) (z N w N) (v N u N)) → ([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ (x ·N w) <N (y ·N z)))
4315, 26, 16caovcld 5596 . . . . 5 (((x N y N) (z N w N) (v N u N)) → (v ·N x) N)
4415, 27, 19caovcld 5596 . . . . 5 (((x N y N) (z N w N) (v N u N)) → (u ·N y) N)
4515, 26, 20caovcld 5596 . . . . 5 (((x N y N) (z N w N) (v N u N)) → (v ·N z) N)
4615, 27, 17caovcld 5596 . . . . 5 (((x N y N) (z N w N) (v N u N)) → (u ·N w) N)
47 ordpipqqs 6358 . . . . 5 ((((v ·N x) N (u ·N y) N) ((v ·N z) N (u ·N w) N)) → ([⟨(v ·N x), (u ·N y)⟩] ~Q <Q [⟨(v ·N z), (u ·N w)⟩] ~Q ↔ ((v ·N x) ·N (u ·N w)) <N ((u ·N y) ·N (v ·N z))))
4843, 44, 45, 46, 47syl22anc 1135 . . . 4 (((x N y N) (z N w N) (v N u N)) → ([⟨(v ·N x), (u ·N y)⟩] ~Q <Q [⟨(v ·N z), (u ·N w)⟩] ~Q ↔ ((v ·N x) ·N (u ·N w)) <N ((u ·N y) ·N (v ·N z))))
4940, 42, 483bitr4d 209 . . 3 (((x N y N) (z N w N) (v N u N)) → ([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ [⟨(v ·N x), (u ·N y)⟩] ~Q <Q [⟨(v ·N z), (u ·N w)⟩] ~Q ))
50 mulpipqqs 6357 . . . . . 6 (((v N u N) (x N y N)) → ([⟨v, u⟩] ~Q ·Q [⟨x, y⟩] ~Q ) = [⟨(v ·N x), (u ·N y)⟩] ~Q )
5150ancoms 255 . . . . 5 (((x N y N) (v N u N)) → ([⟨v, u⟩] ~Q ·Q [⟨x, y⟩] ~Q ) = [⟨(v ·N x), (u ·N y)⟩] ~Q )
52513adant2 922 . . . 4 (((x N y N) (z N w N) (v N u N)) → ([⟨v, u⟩] ~Q ·Q [⟨x, y⟩] ~Q ) = [⟨(v ·N x), (u ·N y)⟩] ~Q )
53 mulpipqqs 6357 . . . . . 6 (((v N u N) (z N w N)) → ([⟨v, u⟩] ~Q ·Q [⟨z, w⟩] ~Q ) = [⟨(v ·N z), (u ·N w)⟩] ~Q )
5453ancoms 255 . . . . 5 (((z N w N) (v N u N)) → ([⟨v, u⟩] ~Q ·Q [⟨z, w⟩] ~Q ) = [⟨(v ·N z), (u ·N w)⟩] ~Q )
55543adant1 921 . . . 4 (((x N y N) (z N w N) (v N u N)) → ([⟨v, u⟩] ~Q ·Q [⟨z, w⟩] ~Q ) = [⟨(v ·N z), (u ·N w)⟩] ~Q )
5652, 55breq12d 3768 . . 3 (((x N y N) (z N w N) (v N u N)) → (([⟨v, u⟩] ~Q ·Q [⟨x, y⟩] ~Q ) <Q ([⟨v, u⟩] ~Q ·Q [⟨z, w⟩] ~Q ) ↔ [⟨(v ·N x), (u ·N y)⟩] ~Q <Q [⟨(v ·N z), (u ·N w)⟩] ~Q ))
5749, 56bitr4d 180 . 2 (((x N y N) (z N w N) (v N u N)) → ([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ ([⟨v, u⟩] ~Q ·Q [⟨x, y⟩] ~Q ) <Q ([⟨v, u⟩] ~Q ·Q [⟨z, w⟩] ~Q )))
581, 5, 9, 13, 573ecoptocl 6131 1 ((A Q B Q 𝐶 Q) → (A <Q B ↔ (𝐶 ·Q A) <Q (𝐶 ·Q B)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 884   = wceq 1242   ∈ wcel 1390  ⟨cop 3370   class class class wbr 3755  (class class class)co 5455  [cec 6040  Ncnpi 6256   ·N cmi 6258
 Copyright terms: Public domain W3C validator