This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐶 ) )