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

Theorem ltanqg 6384
 Description: Ordering property of addition for positive fractions. Proposition 9-2.6(ii) of [Gleason] p. 120. (Contributed by Jim Kingdon, 22-Sep-2019.)
Assertion
Ref Expression
ltanqg ((A Q B Q 𝐶 Q) → (A <Q B ↔ (𝐶 +Q A) <Q (𝐶 +Q B)))

Proof of Theorem ltanqg
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 addclpi 6311 . . . . . 6 ((f N g N) → (f +N g) N)
1514adantl 262 . . . . 5 ((((x N y N) (z N w N) (v N u N)) (f N g N)) → (f +N g) N)
16 simp3l 931 . . . . . 6 (((x N y N) (z N w N) (v N u N)) → v N)
17 simp1r 928 . . . . . 6 (((x N y N) (z N w N) (v N u N)) → y N)
18 mulclpi 6312 . . . . . 6 ((v N y N) → (v ·N y) N)
1916, 17, 18syl2anc 391 . . . . 5 (((x N y N) (z N w N) (v N u N)) → (v ·N y) N)
20 simp3r 932 . . . . . 6 (((x N y N) (z N w N) (v N u N)) → u N)
21 simp1l 927 . . . . . 6 (((x N y N) (z N w N) (v N u N)) → x N)
22 mulclpi 6312 . . . . . 6 ((u N x N) → (u ·N x) N)
2320, 21, 22syl2anc 391 . . . . 5 (((x N y N) (z N w N) (v N u N)) → (u ·N x) N)
2415, 19, 23caovcld 5596 . . . 4 (((x N y N) (z N w N) (v N u N)) → ((v ·N y) +N (u ·N x)) N)
25 mulclpi 6312 . . . . 5 ((u N y N) → (u ·N y) N)
2620, 17, 25syl2anc 391 . . . 4 (((x N y N) (z N w N) (v N u N)) → (u ·N y) N)
27 mulclpi 6312 . . . . . . 7 ((f N g N) → (f ·N g) N)
2827adantl 262 . . . . . 6 ((((x N y N) (z N w N) (v N u N)) (f N g N)) → (f ·N g) N)
29 simp2r 930 . . . . . 6 (((x N y N) (z N w N) (v N u N)) → w N)
3028, 16, 29caovcld 5596 . . . . 5 (((x N y N) (z N w N) (v N u N)) → (v ·N w) N)
31 simp2l 929 . . . . . 6 (((x N y N) (z N w N) (v N u N)) → z N)
32 mulclpi 6312 . . . . . 6 ((u N z N) → (u ·N z) N)
3320, 31, 32syl2anc 391 . . . . 5 (((x N y N) (z N w N) (v N u N)) → (u ·N z) N)
3415, 30, 33caovcld 5596 . . . 4 (((x N y N) (z N w N) (v N u N)) → ((v ·N w) +N (u ·N z)) N)
35 mulclpi 6312 . . . . 5 ((u N w N) → (u ·N w) N)
3620, 29, 35syl2anc 391 . . . 4 (((x N y N) (z N w N) (v N u N)) → (u ·N w) N)
37 ordpipqqs 6358 . . . 4 (((((v ·N y) +N (u ·N x)) N (u ·N y) N) (((v ·N w) +N (u ·N z)) N (u ·N w) N)) → ([⟨((v ·N y) +N (u ·N x)), (u ·N y)⟩] ~Q <Q [⟨((v ·N w) +N (u ·N z)), (u ·N w)⟩] ~Q ↔ (((v ·N y) +N (u ·N x)) ·N (u ·N w)) <N ((u ·N y) ·N ((v ·N w) +N (u ·N z)))))
3824, 26, 34, 36, 37syl22anc 1135 . . 3 (((x N y N) (z N w N) (v N u N)) → ([⟨((v ·N y) +N (u ·N x)), (u ·N y)⟩] ~Q <Q [⟨((v ·N w) +N (u ·N z)), (u ·N w)⟩] ~Q ↔ (((v ·N y) +N (u ·N x)) ·N (u ·N w)) <N ((u ·N y) ·N ((v ·N w) +N (u ·N z)))))
39 simp3 905 . . . . 5 (((x N y N) (z N w N) (v N u N)) → (v N u N))
40 simp1 903 . . . . 5 (((x N y N) (z N w N) (v N u N)) → (x N y N))
41 addpipqqs 6354 . . . . 5 (((v N u N) (x N y N)) → ([⟨v, u⟩] ~Q +Q [⟨x, y⟩] ~Q ) = [⟨((v ·N y) +N (u ·N x)), (u ·N y)⟩] ~Q )
4239, 40, 41syl2anc 391 . . . 4 (((x N y N) (z N w N) (v N u N)) → ([⟨v, u⟩] ~Q +Q [⟨x, y⟩] ~Q ) = [⟨((v ·N y) +N (u ·N x)), (u ·N y)⟩] ~Q )
43 simp2 904 . . . . 5 (((x N y N) (z N w N) (v N u N)) → (z N w N))
44 addpipqqs 6354 . . . . 5 (((v N u N) (z N w N)) → ([⟨v, u⟩] ~Q +Q [⟨z, w⟩] ~Q ) = [⟨((v ·N w) +N (u ·N z)), (u ·N w)⟩] ~Q )
4539, 43, 44syl2anc 391 . . . 4 (((x N y N) (z N w N) (v N u N)) → ([⟨v, u⟩] ~Q +Q [⟨z, w⟩] ~Q ) = [⟨((v ·N w) +N (u ·N z)), (u ·N w)⟩] ~Q )
4642, 45breq12d 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 y) +N (u ·N x)), (u ·N y)⟩] ~Q <Q [⟨((v ·N w) +N (u ·N z)), (u ·N w)⟩] ~Q ))
47 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)))
48473adant3 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)))
49 mulclpi 6312 . . . . . 6 ((x N w N) → (x ·N w) N)
5021, 29, 49syl2anc 391 . . . . 5 (((x N y N) (z N w N) (v N u N)) → (x ·N w) N)
51 mulclpi 6312 . . . . . 6 ((y N z N) → (y ·N z) N)
5217, 31, 51syl2anc 391 . . . . 5 (((x N y N) (z N w N) (v N u N)) → (y ·N z) N)
53 mulclpi 6312 . . . . . 6 ((u N u N) → (u ·N u) N)
5420, 20, 53syl2anc 391 . . . . 5 (((x N y N) (z N w N) (v N u N)) → (u ·N u) N)
55 ltmpig 6323 . . . . 5 (((x ·N w) N (y ·N z) N (u ·N u) N) → ((x ·N w) <N (y ·N z) ↔ ((u ·N u) ·N (x ·N w)) <N ((u ·N u) ·N (y ·N z))))
5650, 52, 54, 55syl3anc 1134 . . . 4 (((x N y N) (z N w N) (v N u N)) → ((x ·N w) <N (y ·N z) ↔ ((u ·N u) ·N (x ·N w)) <N ((u ·N u) ·N (y ·N z))))
57 mulclpi 6312 . . . . . . 7 (((u ·N x) N (u ·N w) N) → ((u ·N x) ·N (u ·N w)) N)
5823, 36, 57syl2anc 391 . . . . . 6 (((x N y N) (z N w N) (v N u N)) → ((u ·N x) ·N (u ·N w)) N)
59 mulclpi 6312 . . . . . . 7 (((u ·N y) N (u ·N z) N) → ((u ·N y) ·N (u ·N z)) N)
6026, 33, 59syl2anc 391 . . . . . 6 (((x N y N) (z N w N) (v N u N)) → ((u ·N y) ·N (u ·N z)) N)
61 mulclpi 6312 . . . . . . 7 (((v ·N y) N (u ·N w) N) → ((v ·N y) ·N (u ·N w)) N)
6219, 36, 61syl2anc 391 . . . . . 6 (((x N y N) (z N w N) (v N u N)) → ((v ·N y) ·N (u ·N w)) N)
63 ltapig 6322 . . . . . 6 ((((u ·N x) ·N (u ·N w)) N ((u ·N y) ·N (u ·N z)) N ((v ·N y) ·N (u ·N w)) N) → (((u ·N x) ·N (u ·N w)) <N ((u ·N y) ·N (u ·N z)) ↔ (((v ·N y) ·N (u ·N w)) +N ((u ·N x) ·N (u ·N w))) <N (((v ·N y) ·N (u ·N w)) +N ((u ·N y) ·N (u ·N z)))))
6458, 60, 62, 63syl3anc 1134 . . . . 5 (((x N y N) (z N w N) (v N u N)) → (((u ·N x) ·N (u ·N w)) <N ((u ·N y) ·N (u ·N z)) ↔ (((v ·N y) ·N (u ·N w)) +N ((u ·N x) ·N (u ·N w))) <N (((v ·N y) ·N (u ·N w)) +N ((u ·N y) ·N (u ·N z)))))
65 mulcompig 6315 . . . . . . . 8 ((f N g N) → (f ·N g) = (g ·N f))
6665adantl 262 . . . . . . 7 ((((x N y N) (z N w N) (v N u N)) (f N g N)) → (f ·N g) = (g ·N f))
67 mulasspig 6316 . . . . . . . 8 ((f N g N N) → ((f ·N g) ·N ) = (f ·N (g ·N )))
6867adantl 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 )))
6920, 20, 21, 66, 68, 29, 28caov4d 5627 . . . . . 6 (((x N y N) (z N w N) (v N u N)) → ((u ·N u) ·N (x ·N w)) = ((u ·N x) ·N (u ·N w)))
7020, 20, 17, 66, 68, 31, 28caov4d 5627 . . . . . 6 (((x N y N) (z N w N) (v N u N)) → ((u ·N u) ·N (y ·N z)) = ((u ·N y) ·N (u ·N z)))
7169, 70breq12d 3768 . . . . 5 (((x N y N) (z N w N) (v N u N)) → (((u ·N u) ·N (x ·N w)) <N ((u ·N u) ·N (y ·N z)) ↔ ((u ·N x) ·N (u ·N w)) <N ((u ·N y) ·N (u ·N z))))
72 distrpig 6317 . . . . . . . 8 ((f N g N N) → (f ·N (g +N )) = ((f ·N g) +N (f ·N )))
7372adantl 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 (f ·N )))
7473, 19, 23, 36, 15, 66caovdir2d 5619 . . . . . 6 (((x N y N) (z N w N) (v N u N)) → (((v ·N y) +N (u ·N x)) ·N (u ·N w)) = (((v ·N y) ·N (u ·N w)) +N ((u ·N x) ·N (u ·N w))))
7573, 26, 30, 33caovdid 5618 . . . . . . 7 (((x N y N) (z N w N) (v N u N)) → ((u ·N y) ·N ((v ·N w) +N (u ·N z))) = (((u ·N y) ·N (v ·N w)) +N ((u ·N y) ·N (u ·N z))))
7620, 17, 16, 66, 68, 29, 28caov411d 5628 . . . . . . . 8 (((x N y N) (z N w N) (v N u N)) → ((u ·N y) ·N (v ·N w)) = ((v ·N y) ·N (u ·N w)))
7776oveq1d 5470 . . . . . . 7 (((x N y N) (z N w N) (v N u N)) → (((u ·N y) ·N (v ·N w)) +N ((u ·N y) ·N (u ·N z))) = (((v ·N y) ·N (u ·N w)) +N ((u ·N y) ·N (u ·N z))))
7875, 77eqtrd 2069 . . . . . 6 (((x N y N) (z N w N) (v N u N)) → ((u ·N y) ·N ((v ·N w) +N (u ·N z))) = (((v ·N y) ·N (u ·N w)) +N ((u ·N y) ·N (u ·N z))))
7974, 78breq12d 3768 . . . . 5 (((x N y N) (z N w N) (v N u N)) → ((((v ·N y) +N (u ·N x)) ·N (u ·N w)) <N ((u ·N y) ·N ((v ·N w) +N (u ·N z))) ↔ (((v ·N y) ·N (u ·N w)) +N ((u ·N x) ·N (u ·N w))) <N (((v ·N y) ·N (u ·N w)) +N ((u ·N y) ·N (u ·N z)))))
8064, 71, 793bitr4d 209 . . . 4 (((x N y N) (z N w N) (v N u N)) → (((u ·N u) ·N (x ·N w)) <N ((u ·N u) ·N (y ·N z)) ↔ (((v ·N y) +N (u ·N x)) ·N (u ·N w)) <N ((u ·N y) ·N ((v ·N w) +N (u ·N z)))))
8148, 56, 803bitrd 203 . . 3 (((x N y N) (z N w N) (v N u N)) → ([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ (((v ·N y) +N (u ·N x)) ·N (u ·N w)) <N ((u ·N y) ·N ((v ·N w) +N (u ·N z)))))
8238, 46, 813bitr4rd 210 . 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 )))
831, 5, 9, 13, 823ecoptocl 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 cpli 6257   ·N cmi 6258
 Copyright terms: Public domain W3C validator