Step |
Hyp |
Ref |
Expression |
1 |
|
id |
⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 ) |
2 |
|
oveq1 |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 +Q 𝑦 ) = ( 𝐴 +Q 𝑦 ) ) |
3 |
1 2
|
breq12d |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 <Q ( 𝑥 +Q 𝑦 ) ↔ 𝐴 <Q ( 𝐴 +Q 𝑦 ) ) ) |
4 |
|
oveq2 |
⊢ ( 𝑦 = 𝐵 → ( 𝐴 +Q 𝑦 ) = ( 𝐴 +Q 𝐵 ) ) |
5 |
4
|
breq2d |
⊢ ( 𝑦 = 𝐵 → ( 𝐴 <Q ( 𝐴 +Q 𝑦 ) ↔ 𝐴 <Q ( 𝐴 +Q 𝐵 ) ) ) |
6 |
|
1lt2nq |
⊢ 1Q <Q ( 1Q +Q 1Q ) |
7 |
|
ltmnq |
⊢ ( 𝑦 ∈ Q → ( 1Q <Q ( 1Q +Q 1Q ) ↔ ( 𝑦 ·Q 1Q ) <Q ( 𝑦 ·Q ( 1Q +Q 1Q ) ) ) ) |
8 |
6 7
|
mpbii |
⊢ ( 𝑦 ∈ Q → ( 𝑦 ·Q 1Q ) <Q ( 𝑦 ·Q ( 1Q +Q 1Q ) ) ) |
9 |
|
mulidnq |
⊢ ( 𝑦 ∈ Q → ( 𝑦 ·Q 1Q ) = 𝑦 ) |
10 |
|
distrnq |
⊢ ( 𝑦 ·Q ( 1Q +Q 1Q ) ) = ( ( 𝑦 ·Q 1Q ) +Q ( 𝑦 ·Q 1Q ) ) |
11 |
9 9
|
oveq12d |
⊢ ( 𝑦 ∈ Q → ( ( 𝑦 ·Q 1Q ) +Q ( 𝑦 ·Q 1Q ) ) = ( 𝑦 +Q 𝑦 ) ) |
12 |
10 11
|
eqtrid |
⊢ ( 𝑦 ∈ Q → ( 𝑦 ·Q ( 1Q +Q 1Q ) ) = ( 𝑦 +Q 𝑦 ) ) |
13 |
8 9 12
|
3brtr3d |
⊢ ( 𝑦 ∈ Q → 𝑦 <Q ( 𝑦 +Q 𝑦 ) ) |
14 |
|
ltanq |
⊢ ( 𝑥 ∈ Q → ( 𝑦 <Q ( 𝑦 +Q 𝑦 ) ↔ ( 𝑥 +Q 𝑦 ) <Q ( 𝑥 +Q ( 𝑦 +Q 𝑦 ) ) ) ) |
15 |
13 14
|
syl5ib |
⊢ ( 𝑥 ∈ Q → ( 𝑦 ∈ Q → ( 𝑥 +Q 𝑦 ) <Q ( 𝑥 +Q ( 𝑦 +Q 𝑦 ) ) ) ) |
16 |
15
|
imp |
⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑥 +Q 𝑦 ) <Q ( 𝑥 +Q ( 𝑦 +Q 𝑦 ) ) ) |
17 |
|
addcomnq |
⊢ ( 𝑥 +Q 𝑦 ) = ( 𝑦 +Q 𝑥 ) |
18 |
|
vex |
⊢ 𝑥 ∈ V |
19 |
|
vex |
⊢ 𝑦 ∈ V |
20 |
|
addcomnq |
⊢ ( 𝑟 +Q 𝑠 ) = ( 𝑠 +Q 𝑟 ) |
21 |
|
addassnq |
⊢ ( ( 𝑟 +Q 𝑠 ) +Q 𝑡 ) = ( 𝑟 +Q ( 𝑠 +Q 𝑡 ) ) |
22 |
18 19 19 20 21
|
caov12 |
⊢ ( 𝑥 +Q ( 𝑦 +Q 𝑦 ) ) = ( 𝑦 +Q ( 𝑥 +Q 𝑦 ) ) |
23 |
16 17 22
|
3brtr3g |
⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑦 +Q 𝑥 ) <Q ( 𝑦 +Q ( 𝑥 +Q 𝑦 ) ) ) |
24 |
|
ltanq |
⊢ ( 𝑦 ∈ Q → ( 𝑥 <Q ( 𝑥 +Q 𝑦 ) ↔ ( 𝑦 +Q 𝑥 ) <Q ( 𝑦 +Q ( 𝑥 +Q 𝑦 ) ) ) ) |
25 |
24
|
adantl |
⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑥 <Q ( 𝑥 +Q 𝑦 ) ↔ ( 𝑦 +Q 𝑥 ) <Q ( 𝑦 +Q ( 𝑥 +Q 𝑦 ) ) ) ) |
26 |
23 25
|
mpbird |
⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → 𝑥 <Q ( 𝑥 +Q 𝑦 ) ) |
27 |
3 5 26
|
vtocl2ga |
⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → 𝐴 <Q ( 𝐴 +Q 𝐵 ) ) |