Metamath Proof Explorer


Theorem prub

Description: A positive fraction not in a positive real is an upper bound. Remark (1) of Gleason p. 122. (Contributed by NM, 25-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion prub ( ( ( 𝐴P𝐵𝐴 ) ∧ 𝐶Q ) → ( ¬ 𝐶𝐴𝐵 <Q 𝐶 ) )

Proof

Step Hyp Ref Expression
1 eleq1 ( 𝐵 = 𝐶 → ( 𝐵𝐴𝐶𝐴 ) )
2 1 biimpcd ( 𝐵𝐴 → ( 𝐵 = 𝐶𝐶𝐴 ) )
3 2 adantl ( ( 𝐴P𝐵𝐴 ) → ( 𝐵 = 𝐶𝐶𝐴 ) )
4 prcdnq ( ( 𝐴P𝐵𝐴 ) → ( 𝐶 <Q 𝐵𝐶𝐴 ) )
5 3 4 jaod ( ( 𝐴P𝐵𝐴 ) → ( ( 𝐵 = 𝐶𝐶 <Q 𝐵 ) → 𝐶𝐴 ) )
6 5 con3d ( ( 𝐴P𝐵𝐴 ) → ( ¬ 𝐶𝐴 → ¬ ( 𝐵 = 𝐶𝐶 <Q 𝐵 ) ) )
7 6 adantr ( ( ( 𝐴P𝐵𝐴 ) ∧ 𝐶Q ) → ( ¬ 𝐶𝐴 → ¬ ( 𝐵 = 𝐶𝐶 <Q 𝐵 ) ) )
8 elprnq ( ( 𝐴P𝐵𝐴 ) → 𝐵Q )
9 ltsonq <Q Or Q
10 sotric ( ( <Q Or Q ∧ ( 𝐵Q𝐶Q ) ) → ( 𝐵 <Q 𝐶 ↔ ¬ ( 𝐵 = 𝐶𝐶 <Q 𝐵 ) ) )
11 9 10 mpan ( ( 𝐵Q𝐶Q ) → ( 𝐵 <Q 𝐶 ↔ ¬ ( 𝐵 = 𝐶𝐶 <Q 𝐵 ) ) )
12 8 11 sylan ( ( ( 𝐴P𝐵𝐴 ) ∧ 𝐶Q ) → ( 𝐵 <Q 𝐶 ↔ ¬ ( 𝐵 = 𝐶𝐶 <Q 𝐵 ) ) )
13 7 12 sylibrd ( ( ( 𝐴P𝐵𝐴 ) ∧ 𝐶Q ) → ( ¬ 𝐶𝐴𝐵 <Q 𝐶 ) )