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

Theorem ltanqg 7056
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 ((𝐴Q𝐵Q𝐶Q) → (𝐴 <Q 𝐵 ↔ (𝐶 +Q 𝐴) <Q (𝐶 +Q 𝐵)))

Proof of Theorem ltanqg
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 𝑢 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nqqs 7004 . 2 Q = ((N × N) / ~Q )
2 breq1 3870 . . 3 ([⟨𝑥, 𝑦⟩] ~Q = 𝐴 → ([⟨𝑥, 𝑦⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q𝐴 <Q [⟨𝑧, 𝑤⟩] ~Q ))
3 oveq2 5698 . . . 4 ([⟨𝑥, 𝑦⟩] ~Q = 𝐴 → ([⟨𝑣, 𝑢⟩] ~Q +Q [⟨𝑥, 𝑦⟩] ~Q ) = ([⟨𝑣, 𝑢⟩] ~Q +Q 𝐴))
43breq1d 3877 . . 3 ([⟨𝑥, 𝑦⟩] ~Q = 𝐴 → (([⟨𝑣, 𝑢⟩] ~Q +Q [⟨𝑥, 𝑦⟩] ~Q ) <Q ([⟨𝑣, 𝑢⟩] ~Q +Q [⟨𝑧, 𝑤⟩] ~Q ) ↔ ([⟨𝑣, 𝑢⟩] ~Q +Q 𝐴) <Q ([⟨𝑣, 𝑢⟩] ~Q +Q [⟨𝑧, 𝑤⟩] ~Q )))
52, 4bibi12d 234 . 2 ([⟨𝑥, 𝑦⟩] ~Q = 𝐴 → (([⟨𝑥, 𝑦⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ ([⟨𝑣, 𝑢⟩] ~Q +Q [⟨𝑥, 𝑦⟩] ~Q ) <Q ([⟨𝑣, 𝑢⟩] ~Q +Q [⟨𝑧, 𝑤⟩] ~Q )) ↔ (𝐴 <Q [⟨𝑧, 𝑤⟩] ~Q ↔ ([⟨𝑣, 𝑢⟩] ~Q +Q 𝐴) <Q ([⟨𝑣, 𝑢⟩] ~Q +Q [⟨𝑧, 𝑤⟩] ~Q ))))
6 breq2 3871 . . 3 ([⟨𝑧, 𝑤⟩] ~Q = 𝐵 → (𝐴 <Q [⟨𝑧, 𝑤⟩] ~Q𝐴 <Q 𝐵))
7 oveq2 5698 . . . 4 ([⟨𝑧, 𝑤⟩] ~Q = 𝐵 → ([⟨𝑣, 𝑢⟩] ~Q +Q [⟨𝑧, 𝑤⟩] ~Q ) = ([⟨𝑣, 𝑢⟩] ~Q +Q 𝐵))
87breq2d 3879 . . 3 ([⟨𝑧, 𝑤⟩] ~Q = 𝐵 → (([⟨𝑣, 𝑢⟩] ~Q +Q 𝐴) <Q ([⟨𝑣, 𝑢⟩] ~Q +Q [⟨𝑧, 𝑤⟩] ~Q ) ↔ ([⟨𝑣, 𝑢⟩] ~Q +Q 𝐴) <Q ([⟨𝑣, 𝑢⟩] ~Q +Q 𝐵)))
96, 8bibi12d 234 . 2 ([⟨𝑧, 𝑤⟩] ~Q = 𝐵 → ((𝐴 <Q [⟨𝑧, 𝑤⟩] ~Q ↔ ([⟨𝑣, 𝑢⟩] ~Q +Q 𝐴) <Q ([⟨𝑣, 𝑢⟩] ~Q +Q [⟨𝑧, 𝑤⟩] ~Q )) ↔ (𝐴 <Q 𝐵 ↔ ([⟨𝑣, 𝑢⟩] ~Q +Q 𝐴) <Q ([⟨𝑣, 𝑢⟩] ~Q +Q 𝐵))))
10 oveq1 5697 . . . 4 ([⟨𝑣, 𝑢⟩] ~Q = 𝐶 → ([⟨𝑣, 𝑢⟩] ~Q +Q 𝐴) = (𝐶 +Q 𝐴))
11 oveq1 5697 . . . 4 ([⟨𝑣, 𝑢⟩] ~Q = 𝐶 → ([⟨𝑣, 𝑢⟩] ~Q +Q 𝐵) = (𝐶 +Q 𝐵))
1210, 11breq12d 3880 . . 3 ([⟨𝑣, 𝑢⟩] ~Q = 𝐶 → (([⟨𝑣, 𝑢⟩] ~Q +Q 𝐴) <Q ([⟨𝑣, 𝑢⟩] ~Q +Q 𝐵) ↔ (𝐶 +Q 𝐴) <Q (𝐶 +Q 𝐵)))
1312bibi2d 231 . 2 ([⟨𝑣, 𝑢⟩] ~Q = 𝐶 → ((𝐴 <Q 𝐵 ↔ ([⟨𝑣, 𝑢⟩] ~Q +Q 𝐴) <Q ([⟨𝑣, 𝑢⟩] ~Q +Q 𝐵)) ↔ (𝐴 <Q 𝐵 ↔ (𝐶 +Q 𝐴) <Q (𝐶 +Q 𝐵))))
14 addclpi 6983 . . . . . 6 ((𝑓N𝑔N) → (𝑓 +N 𝑔) ∈ N)
1514adantl 272 . . . . 5 ((((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) ∧ (𝑓N𝑔N)) → (𝑓 +N 𝑔) ∈ N)
16 simp3l 974 . . . . . 6 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → 𝑣N)
17 simp1r 971 . . . . . 6 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → 𝑦N)
18 mulclpi 6984 . . . . . 6 ((𝑣N𝑦N) → (𝑣 ·N 𝑦) ∈ N)
1916, 17, 18syl2anc 404 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (𝑣 ·N 𝑦) ∈ N)
20 simp3r 975 . . . . . 6 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → 𝑢N)
21 simp1l 970 . . . . . 6 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → 𝑥N)
22 mulclpi 6984 . . . . . 6 ((𝑢N𝑥N) → (𝑢 ·N 𝑥) ∈ N)
2320, 21, 22syl2anc 404 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (𝑢 ·N 𝑥) ∈ N)
2415, 19, 23caovcld 5836 . . . 4 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ((𝑣 ·N 𝑦) +N (𝑢 ·N 𝑥)) ∈ N)
25 mulclpi 6984 . . . . 5 ((𝑢N𝑦N) → (𝑢 ·N 𝑦) ∈ N)
2620, 17, 25syl2anc 404 . . . 4 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (𝑢 ·N 𝑦) ∈ N)
27 mulclpi 6984 . . . . . . 7 ((𝑓N𝑔N) → (𝑓 ·N 𝑔) ∈ N)
2827adantl 272 . . . . . 6 ((((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) ∧ (𝑓N𝑔N)) → (𝑓 ·N 𝑔) ∈ N)
29 simp2r 973 . . . . . 6 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → 𝑤N)
3028, 16, 29caovcld 5836 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (𝑣 ·N 𝑤) ∈ N)
31 simp2l 972 . . . . . 6 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → 𝑧N)
32 mulclpi 6984 . . . . . 6 ((𝑢N𝑧N) → (𝑢 ·N 𝑧) ∈ N)
3320, 31, 32syl2anc 404 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (𝑢 ·N 𝑧) ∈ N)
3415, 30, 33caovcld 5836 . . . 4 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ((𝑣 ·N 𝑤) +N (𝑢 ·N 𝑧)) ∈ N)
35 mulclpi 6984 . . . . 5 ((𝑢N𝑤N) → (𝑢 ·N 𝑤) ∈ N)
3620, 29, 35syl2anc 404 . . . 4 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (𝑢 ·N 𝑤) ∈ N)
37 ordpipqqs 7030 . . . 4 (((((𝑣 ·N 𝑦) +N (𝑢 ·N 𝑥)) ∈ N ∧ (𝑢 ·N 𝑦) ∈ N) ∧ (((𝑣 ·N 𝑤) +N (𝑢 ·N 𝑧)) ∈ N ∧ (𝑢 ·N 𝑤) ∈ N)) → ([⟨((𝑣 ·N 𝑦) +N (𝑢 ·N 𝑥)), (𝑢 ·N 𝑦)⟩] ~Q <Q [⟨((𝑣 ·N 𝑤) +N (𝑢 ·N 𝑧)), (𝑢 ·N 𝑤)⟩] ~Q ↔ (((𝑣 ·N 𝑦) +N (𝑢 ·N 𝑥)) ·N (𝑢 ·N 𝑤)) <N ((𝑢 ·N 𝑦) ·N ((𝑣 ·N 𝑤) +N (𝑢 ·N 𝑧)))))
3824, 26, 34, 36, 37syl22anc 1182 . . 3 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ([⟨((𝑣 ·N 𝑦) +N (𝑢 ·N 𝑥)), (𝑢 ·N 𝑦)⟩] ~Q <Q [⟨((𝑣 ·N 𝑤) +N (𝑢 ·N 𝑧)), (𝑢 ·N 𝑤)⟩] ~Q ↔ (((𝑣 ·N 𝑦) +N (𝑢 ·N 𝑥)) ·N (𝑢 ·N 𝑤)) <N ((𝑢 ·N 𝑦) ·N ((𝑣 ·N 𝑤) +N (𝑢 ·N 𝑧)))))
39 simp3 948 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (𝑣N𝑢N))
40 simp1 946 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (𝑥N𝑦N))
41 addpipqqs 7026 . . . . 5 (((𝑣N𝑢N) ∧ (𝑥N𝑦N)) → ([⟨𝑣, 𝑢⟩] ~Q +Q [⟨𝑥, 𝑦⟩] ~Q ) = [⟨((𝑣 ·N 𝑦) +N (𝑢 ·N 𝑥)), (𝑢 ·N 𝑦)⟩] ~Q )
4239, 40, 41syl2anc 404 . . . 4 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ([⟨𝑣, 𝑢⟩] ~Q +Q [⟨𝑥, 𝑦⟩] ~Q ) = [⟨((𝑣 ·N 𝑦) +N (𝑢 ·N 𝑥)), (𝑢 ·N 𝑦)⟩] ~Q )
43 simp2 947 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (𝑧N𝑤N))
44 addpipqqs 7026 . . . . 5 (((𝑣N𝑢N) ∧ (𝑧N𝑤N)) → ([⟨𝑣, 𝑢⟩] ~Q +Q [⟨𝑧, 𝑤⟩] ~Q ) = [⟨((𝑣 ·N 𝑤) +N (𝑢 ·N 𝑧)), (𝑢 ·N 𝑤)⟩] ~Q )
4539, 43, 44syl2anc 404 . . . 4 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ([⟨𝑣, 𝑢⟩] ~Q +Q [⟨𝑧, 𝑤⟩] ~Q ) = [⟨((𝑣 ·N 𝑤) +N (𝑢 ·N 𝑧)), (𝑢 ·N 𝑤)⟩] ~Q )
4642, 45breq12d 3880 . . 3 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (([⟨𝑣, 𝑢⟩] ~Q +Q [⟨𝑥, 𝑦⟩] ~Q ) <Q ([⟨𝑣, 𝑢⟩] ~Q +Q [⟨𝑧, 𝑤⟩] ~Q ) ↔ [⟨((𝑣 ·N 𝑦) +N (𝑢 ·N 𝑥)), (𝑢 ·N 𝑦)⟩] ~Q <Q [⟨((𝑣 ·N 𝑤) +N (𝑢 ·N 𝑧)), (𝑢 ·N 𝑤)⟩] ~Q ))
47 ordpipqqs 7030 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N)) → ([⟨𝑥, 𝑦⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ (𝑥 ·N 𝑤) <N (𝑦 ·N 𝑧)))
48473adant3 966 . . . 4 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ([⟨𝑥, 𝑦⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ (𝑥 ·N 𝑤) <N (𝑦 ·N 𝑧)))
49 mulclpi 6984 . . . . . 6 ((𝑥N𝑤N) → (𝑥 ·N 𝑤) ∈ N)
5021, 29, 49syl2anc 404 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (𝑥 ·N 𝑤) ∈ N)
51 mulclpi 6984 . . . . . 6 ((𝑦N𝑧N) → (𝑦 ·N 𝑧) ∈ N)
5217, 31, 51syl2anc 404 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (𝑦 ·N 𝑧) ∈ N)
53 mulclpi 6984 . . . . . 6 ((𝑢N𝑢N) → (𝑢 ·N 𝑢) ∈ N)
5420, 20, 53syl2anc 404 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (𝑢 ·N 𝑢) ∈ N)
55 ltmpig 6995 . . . . 5 (((𝑥 ·N 𝑤) ∈ N ∧ (𝑦 ·N 𝑧) ∈ N ∧ (𝑢 ·N 𝑢) ∈ N) → ((𝑥 ·N 𝑤) <N (𝑦 ·N 𝑧) ↔ ((𝑢 ·N 𝑢) ·N (𝑥 ·N 𝑤)) <N ((𝑢 ·N 𝑢) ·N (𝑦 ·N 𝑧))))
5650, 52, 54, 55syl3anc 1181 . . . 4 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ((𝑥 ·N 𝑤) <N (𝑦 ·N 𝑧) ↔ ((𝑢 ·N 𝑢) ·N (𝑥 ·N 𝑤)) <N ((𝑢 ·N 𝑢) ·N (𝑦 ·N 𝑧))))
57 mulclpi 6984 . . . . . . 7 (((𝑢 ·N 𝑥) ∈ N ∧ (𝑢 ·N 𝑤) ∈ N) → ((𝑢 ·N 𝑥) ·N (𝑢 ·N 𝑤)) ∈ N)
5823, 36, 57syl2anc 404 . . . . . 6 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ((𝑢 ·N 𝑥) ·N (𝑢 ·N 𝑤)) ∈ N)
59 mulclpi 6984 . . . . . . 7 (((𝑢 ·N 𝑦) ∈ N ∧ (𝑢 ·N 𝑧) ∈ N) → ((𝑢 ·N 𝑦) ·N (𝑢 ·N 𝑧)) ∈ N)
6026, 33, 59syl2anc 404 . . . . . 6 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ((𝑢 ·N 𝑦) ·N (𝑢 ·N 𝑧)) ∈ N)
61 mulclpi 6984 . . . . . . 7 (((𝑣 ·N 𝑦) ∈ N ∧ (𝑢 ·N 𝑤) ∈ N) → ((𝑣 ·N 𝑦) ·N (𝑢 ·N 𝑤)) ∈ N)
6219, 36, 61syl2anc 404 . . . . . 6 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ((𝑣 ·N 𝑦) ·N (𝑢 ·N 𝑤)) ∈ N)
63 ltapig 6994 . . . . . 6 ((((𝑢 ·N 𝑥) ·N (𝑢 ·N 𝑤)) ∈ N ∧ ((𝑢 ·N 𝑦) ·N (𝑢 ·N 𝑧)) ∈ N ∧ ((𝑣 ·N 𝑦) ·N (𝑢 ·N 𝑤)) ∈ N) → (((𝑢 ·N 𝑥) ·N (𝑢 ·N 𝑤)) <N ((𝑢 ·N 𝑦) ·N (𝑢 ·N 𝑧)) ↔ (((𝑣 ·N 𝑦) ·N (𝑢 ·N 𝑤)) +N ((𝑢 ·N 𝑥) ·N (𝑢 ·N 𝑤))) <N (((𝑣 ·N 𝑦) ·N (𝑢 ·N 𝑤)) +N ((𝑢 ·N 𝑦) ·N (𝑢 ·N 𝑧)))))
6458, 60, 62, 63syl3anc 1181 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (((𝑢 ·N 𝑥) ·N (𝑢 ·N 𝑤)) <N ((𝑢 ·N 𝑦) ·N (𝑢 ·N 𝑧)) ↔ (((𝑣 ·N 𝑦) ·N (𝑢 ·N 𝑤)) +N ((𝑢 ·N 𝑥) ·N (𝑢 ·N 𝑤))) <N (((𝑣 ·N 𝑦) ·N (𝑢 ·N 𝑤)) +N ((𝑢 ·N 𝑦) ·N (𝑢 ·N 𝑧)))))
65 mulcompig 6987 . . . . . . . 8 ((𝑓N𝑔N) → (𝑓 ·N 𝑔) = (𝑔 ·N 𝑓))
6665adantl 272 . . . . . . 7 ((((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) ∧ (𝑓N𝑔N)) → (𝑓 ·N 𝑔) = (𝑔 ·N 𝑓))
67 mulasspig 6988 . . . . . . . 8 ((𝑓N𝑔NN) → ((𝑓 ·N 𝑔) ·N ) = (𝑓 ·N (𝑔 ·N )))
6867adantl 272 . . . . . . 7 ((((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) ∧ (𝑓N𝑔NN)) → ((𝑓 ·N 𝑔) ·N ) = (𝑓 ·N (𝑔 ·N )))
6920, 20, 21, 66, 68, 29, 28caov4d 5867 . . . . . 6 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ((𝑢 ·N 𝑢) ·N (𝑥 ·N 𝑤)) = ((𝑢 ·N 𝑥) ·N (𝑢 ·N 𝑤)))
7020, 20, 17, 66, 68, 31, 28caov4d 5867 . . . . . 6 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ((𝑢 ·N 𝑢) ·N (𝑦 ·N 𝑧)) = ((𝑢 ·N 𝑦) ·N (𝑢 ·N 𝑧)))
7169, 70breq12d 3880 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (((𝑢 ·N 𝑢) ·N (𝑥 ·N 𝑤)) <N ((𝑢 ·N 𝑢) ·N (𝑦 ·N 𝑧)) ↔ ((𝑢 ·N 𝑥) ·N (𝑢 ·N 𝑤)) <N ((𝑢 ·N 𝑦) ·N (𝑢 ·N 𝑧))))
72 distrpig 6989 . . . . . . . 8 ((𝑓N𝑔NN) → (𝑓 ·N (𝑔 +N )) = ((𝑓 ·N 𝑔) +N (𝑓 ·N )))
7372adantl 272 . . . . . . 7 ((((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) ∧ (𝑓N𝑔NN)) → (𝑓 ·N (𝑔 +N )) = ((𝑓 ·N 𝑔) +N (𝑓 ·N )))
7473, 19, 23, 36, 15, 66caovdir2d 5859 . . . . . 6 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (((𝑣 ·N 𝑦) +N (𝑢 ·N 𝑥)) ·N (𝑢 ·N 𝑤)) = (((𝑣 ·N 𝑦) ·N (𝑢 ·N 𝑤)) +N ((𝑢 ·N 𝑥) ·N (𝑢 ·N 𝑤))))
7573, 26, 30, 33caovdid 5858 . . . . . . 7 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ((𝑢 ·N 𝑦) ·N ((𝑣 ·N 𝑤) +N (𝑢 ·N 𝑧))) = (((𝑢 ·N 𝑦) ·N (𝑣 ·N 𝑤)) +N ((𝑢 ·N 𝑦) ·N (𝑢 ·N 𝑧))))
7620, 17, 16, 66, 68, 29, 28caov411d 5868 . . . . . . . 8 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ((𝑢 ·N 𝑦) ·N (𝑣 ·N 𝑤)) = ((𝑣 ·N 𝑦) ·N (𝑢 ·N 𝑤)))
7776oveq1d 5705 . . . . . . 7 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (((𝑢 ·N 𝑦) ·N (𝑣 ·N 𝑤)) +N ((𝑢 ·N 𝑦) ·N (𝑢 ·N 𝑧))) = (((𝑣 ·N 𝑦) ·N (𝑢 ·N 𝑤)) +N ((𝑢 ·N 𝑦) ·N (𝑢 ·N 𝑧))))
7875, 77eqtrd 2127 . . . . . 6 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ((𝑢 ·N 𝑦) ·N ((𝑣 ·N 𝑤) +N (𝑢 ·N 𝑧))) = (((𝑣 ·N 𝑦) ·N (𝑢 ·N 𝑤)) +N ((𝑢 ·N 𝑦) ·N (𝑢 ·N 𝑧))))
7974, 78breq12d 3880 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ((((𝑣 ·N 𝑦) +N (𝑢 ·N 𝑥)) ·N (𝑢 ·N 𝑤)) <N ((𝑢 ·N 𝑦) ·N ((𝑣 ·N 𝑤) +N (𝑢 ·N 𝑧))) ↔ (((𝑣 ·N 𝑦) ·N (𝑢 ·N 𝑤)) +N ((𝑢 ·N 𝑥) ·N (𝑢 ·N 𝑤))) <N (((𝑣 ·N 𝑦) ·N (𝑢 ·N 𝑤)) +N ((𝑢 ·N 𝑦) ·N (𝑢 ·N 𝑧)))))
8064, 71, 793bitr4d 219 . . . 4 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → (((𝑢 ·N 𝑢) ·N (𝑥 ·N 𝑤)) <N ((𝑢 ·N 𝑢) ·N (𝑦 ·N 𝑧)) ↔ (((𝑣 ·N 𝑦) +N (𝑢 ·N 𝑥)) ·N (𝑢 ·N 𝑤)) <N ((𝑢 ·N 𝑦) ·N ((𝑣 ·N 𝑤) +N (𝑢 ·N 𝑧)))))
8148, 56, 803bitrd 213 . . 3 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ([⟨𝑥, 𝑦⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ (((𝑣 ·N 𝑦) +N (𝑢 ·N 𝑥)) ·N (𝑢 ·N 𝑤)) <N ((𝑢 ·N 𝑦) ·N ((𝑣 ·N 𝑤) +N (𝑢 ·N 𝑧)))))
8238, 46, 813bitr4rd 220 . 2 (((𝑥N𝑦N) ∧ (𝑧N𝑤N) ∧ (𝑣N𝑢N)) → ([⟨𝑥, 𝑦⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ ([⟨𝑣, 𝑢⟩] ~Q +Q [⟨𝑥, 𝑦⟩] ~Q ) <Q ([⟨𝑣, 𝑢⟩] ~Q +Q [⟨𝑧, 𝑤⟩] ~Q )))
831, 5, 9, 13, 823ecoptocl 6421 1 ((𝐴Q𝐵Q𝐶Q) → (𝐴 <Q 𝐵 ↔ (𝐶 +Q 𝐴) <Q (𝐶 +Q 𝐵)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  w3a 927   = wceq 1296  wcel 1445  cop 3469   class class class wbr 3867  (class class class)co 5690  [cec 6330  Ncnpi 6928   +N cpli 6929   ·N cmi 6930   <N clti 6931   ~Q ceq 6935  Qcnq 6936   +Q cplq 6938   <Q cltq 6941
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-13 1456  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-coll 3975  ax-sep 3978  ax-nul 3986  ax-pow 4030  ax-pr 4060  ax-un 4284  ax-setind 4381  ax-iinf 4431
This theorem depends on definitions:  df-bi 116  df-dc 784  df-3or 928  df-3an 929  df-tru 1299  df-fal 1302  df-nf 1402  df-sb 1700  df-eu 1958  df-mo 1959  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ne 2263  df-ral 2375  df-rex 2376  df-reu 2377  df-rab 2379  df-v 2635  df-sbc 2855  df-csb 2948  df-dif 3015  df-un 3017  df-in 3019  df-ss 3026  df-nul 3303  df-pw 3451  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-int 3711  df-iun 3754  df-br 3868  df-opab 3922  df-mpt 3923  df-tr 3959  df-eprel 4140  df-id 4144  df-iord 4217  df-on 4219  df-suc 4222  df-iom 4434  df-xp 4473  df-rel 4474  df-cnv 4475  df-co 4476  df-dm 4477  df-rn 4478  df-res 4479  df-ima 4480  df-iota 5014  df-fun 5051  df-fn 5052  df-f 5053  df-f1 5054  df-fo 5055  df-f1o 5056  df-fv 5057  df-ov 5693  df-oprab 5694  df-mpt2 5695  df-1st 5949  df-2nd 5950  df-recs 6108  df-irdg 6173  df-oadd 6223  df-omul 6224  df-er 6332  df-ec 6334  df-qs 6338  df-ni 6960  df-pli 6961  df-mi 6962  df-lti 6963  df-plpq 7000  df-enq 7003  df-nqqs 7004  df-plqqs 7005  df-ltnqqs 7009
This theorem is referenced by:  ltanqi  7058  lt2addnq  7060  ltaddnq  7063  prarloclemlt  7149  prarloclemcalc  7158  addlocprlemgt  7190  addclpr  7193  prmuloclemcalc  7221  distrlem4prl  7240  distrlem4pru  7241  ltexprlemopl  7257  ltexprlemopu  7259  ltexprlemdisj  7262  ltexprlemloc  7263  ltexprlemfl  7265  ltexprlemfu  7267  aptiprleml  7295  aptiprlemu  7296  cauappcvgprlemopl  7302  cauappcvgprlemlol  7303  cauappcvgprlemdisj  7307  cauappcvgprlemloc  7308  cauappcvgprlemladdfu  7310  cauappcvgprlemladdru  7312  cauappcvgprlemladdrl  7313  cauappcvgprlem1  7315  caucvgprlemnkj  7322  caucvgprlemnbj  7323  caucvgprlemm  7324  caucvgprlemopl  7325  caucvgprlemlol  7326  caucvgprlemloc  7331  caucvgprlemladdfu  7333  caucvgprlemladdrl  7334  caucvgprprlemml  7350  caucvgprprlemopl  7353  caucvgprprlemlol  7354
  Copyright terms: Public domain W3C validator