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