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

Theorem 1lt2nq 6504
 Description: One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.)
Assertion
Ref Expression
1lt2nq 1Q <Q (1Q +Q 1Q)

Proof of Theorem 1lt2nq
StepHypRef Expression
1 1lt2pi 6438 . . . . 5 1𝑜 <N (1𝑜 +N 1𝑜)
2 1pi 6413 . . . . . 6 1𝑜N
3 mulidpi 6416 . . . . . 6 (1𝑜N → (1𝑜 ·N 1𝑜) = 1𝑜)
42, 3ax-mp 7 . . . . 5 (1𝑜 ·N 1𝑜) = 1𝑜
54, 4oveq12i 5524 . . . . 5 ((1𝑜 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)) = (1𝑜 +N 1𝑜)
61, 4, 53brtr4i 3792 . . . 4 (1𝑜 ·N 1𝑜) <N ((1𝑜 ·N 1𝑜) +N (1𝑜 ·N 1𝑜))
7 mulclpi 6426 . . . . . 6 ((1𝑜N ∧ 1𝑜N) → (1𝑜 ·N 1𝑜) ∈ N)
82, 2, 7mp2an 402 . . . . 5 (1𝑜 ·N 1𝑜) ∈ N
9 addclpi 6425 . . . . . 6 (((1𝑜 ·N 1𝑜) ∈ N ∧ (1𝑜 ·N 1𝑜) ∈ N) → ((1𝑜 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)) ∈ N)
108, 8, 9mp2an 402 . . . . 5 ((1𝑜 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)) ∈ N
11 ltmpig 6437 . . . . 5 (((1𝑜 ·N 1𝑜) ∈ N ∧ ((1𝑜 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)) ∈ N ∧ 1𝑜N) → ((1𝑜 ·N 1𝑜) <N ((1𝑜 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)) ↔ (1𝑜 ·N (1𝑜 ·N 1𝑜)) <N (1𝑜 ·N ((1𝑜 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)))))
128, 10, 2, 11mp3an 1232 . . . 4 ((1𝑜 ·N 1𝑜) <N ((1𝑜 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)) ↔ (1𝑜 ·N (1𝑜 ·N 1𝑜)) <N (1𝑜 ·N ((1𝑜 ·N 1𝑜) +N (1𝑜 ·N 1𝑜))))
136, 12mpbi 133 . . 3 (1𝑜 ·N (1𝑜 ·N 1𝑜)) <N (1𝑜 ·N ((1𝑜 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)))
14 ordpipqqs 6472 . . . 4 (((1𝑜N ∧ 1𝑜N) ∧ (((1𝑜 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)) ∈ N ∧ (1𝑜 ·N 1𝑜) ∈ N)) → ([⟨1𝑜, 1𝑜⟩] ~Q <Q [⟨((1𝑜 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)), (1𝑜 ·N 1𝑜)⟩] ~Q ↔ (1𝑜 ·N (1𝑜 ·N 1𝑜)) <N (1𝑜 ·N ((1𝑜 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)))))
152, 2, 10, 8, 14mp4an 403 . . 3 ([⟨1𝑜, 1𝑜⟩] ~Q <Q [⟨((1𝑜 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)), (1𝑜 ·N 1𝑜)⟩] ~Q ↔ (1𝑜 ·N (1𝑜 ·N 1𝑜)) <N (1𝑜 ·N ((1𝑜 ·N 1𝑜) +N (1𝑜 ·N 1𝑜))))
1613, 15mpbir 134 . 2 [⟨1𝑜, 1𝑜⟩] ~Q <Q [⟨((1𝑜 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)), (1𝑜 ·N 1𝑜)⟩] ~Q
17 df-1nqqs 6449 . 2 1Q = [⟨1𝑜, 1𝑜⟩] ~Q
1817, 17oveq12i 5524 . . 3 (1Q +Q 1Q) = ([⟨1𝑜, 1𝑜⟩] ~Q +Q [⟨1𝑜, 1𝑜⟩] ~Q )
19 addpipqqs 6468 . . . 4 (((1𝑜N ∧ 1𝑜N) ∧ (1𝑜N ∧ 1𝑜N)) → ([⟨1𝑜, 1𝑜⟩] ~Q +Q [⟨1𝑜, 1𝑜⟩] ~Q ) = [⟨((1𝑜 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)), (1𝑜 ·N 1𝑜)⟩] ~Q )
202, 2, 2, 2, 19mp4an 403 . . 3 ([⟨1𝑜, 1𝑜⟩] ~Q +Q [⟨1𝑜, 1𝑜⟩] ~Q ) = [⟨((1𝑜 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)), (1𝑜 ·N 1𝑜)⟩] ~Q
2118, 20eqtri 2060 . 2 (1Q +Q 1Q) = [⟨((1𝑜 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)), (1𝑜 ·N 1𝑜)⟩] ~Q
2216, 17, 213brtr4i 3792 1 1Q <Q (1Q +Q 1Q)
 Colors of variables: wff set class Syntax hints:   ↔ wb 98   = wceq 1243   ∈ wcel 1393  ⟨cop 3378   class class class wbr 3764  (class class class)co 5512  1𝑜c1o 5994  [cec 6104  Ncnpi 6370   +N cpli 6371   ·N cmi 6372
 Copyright terms: Public domain W3C validator