Theorem 3pos 9143

Description: The number 3 is positive. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
3pos	⊢ 0 < 3

Proof of Theorem 3pos

Step	Hyp	Ref	Expression
1		2re 9119	. . 3 ⊢ 2 ∈ ℝ
2		1re 8084	. . 3 ⊢ 1 ∈ ℝ
3		2pos 9140	. . 3 ⊢ 0 < 2
4		0lt1 8212	. . 3 ⊢ 0 < 1
5	1, 2, 3, 4	addgt0ii 8577	. 2 ⊢ 0 < (2 + 1)
6		df-3 9109	. 2 ⊢ 3 = (2 + 1)
7	5, 6	breqtrri 4075	1 ⊢ 0 < 3

Syntax hints:   class class class wbr 4048  (class class class)co 5954  0cc0 7938  1c1 7939   + caddc 7941   < clt 8120  2c2 9100  3c3 9101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-sep 4167  ax-pow 4223  ax-pr 4258  ax-un 4485  ax-setind 4590  ax-cnex 8029  ax-resscn 8030  ax-1cn 8031  ax-1re 8032  ax-icn 8033  ax-addcl 8034  ax-addrcl 8035  ax-mulcl 8036  ax-addcom 8038  ax-addass 8040  ax-i2m1 8043  ax-0lt1 8044  ax-0id 8046  ax-rnegex 8047  ax-pre-lttrn 8052  ax-pre-ltadd 8054

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ne 2378  df-nel 2473  df-ral 2490  df-rex 2491  df-rab 2494  df-v 2775  df-dif 3170  df-un 3172  df-in 3174  df-ss 3181  df-pw 3620  df-sn 3641  df-pr 3642  df-op 3644  df-uni 3854  df-br 4049  df-opab 4111  df-xp 4686  df-iota 5238  df-fv 5285  df-ov 5957  df-pnf 8122  df-mnf 8123  df-ltxr 8125  df-2 9108  df-3 9109

This theorem is referenced by:  3ne0  9144  3ap0  9145  4pos  9146  8th4div3  9269  halfpm6th  9270  3rp  9794  fz0to4untppr  10259  sqrt9  11409  ef01bndlem  12117  cos2bnd  12121  sin01gt0  12123  cos01gt0  12124  flodddiv4  12297  slotsdifunifndx  13114  coseq0negpitopi  15358  tangtx  15360  sincos6thpi  15364  cos02pilt1  15373  lgsdir2lem1  15555  ex-gcd  15781