Metamath Proof Explorer


Theorem nnmordi

Description: Ordering property of multiplication. Half of Proposition 8.19 of TakeutiZaring p. 63, limited to natural numbers. (Contributed by NM, 18-Sep-1995) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Assertion nnmordi ( ( ( ๐ต โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โˆง โˆ… โˆˆ ๐ถ ) โ†’ ( ๐ด โˆˆ ๐ต โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐ต ) ) )

Proof

Step Hyp Ref Expression
1 elnn โŠข ( ( ๐ด โˆˆ ๐ต โˆง ๐ต โˆˆ ฯ‰ ) โ†’ ๐ด โˆˆ ฯ‰ )
2 1 expcom โŠข ( ๐ต โˆˆ ฯ‰ โ†’ ( ๐ด โˆˆ ๐ต โ†’ ๐ด โˆˆ ฯ‰ ) )
3 eleq2 โŠข ( ๐‘ฅ = ๐ต โ†’ ( ๐ด โˆˆ ๐‘ฅ โ†” ๐ด โˆˆ ๐ต ) )
4 oveq2 โŠข ( ๐‘ฅ = ๐ต โ†’ ( ๐ถ ยทo ๐‘ฅ ) = ( ๐ถ ยทo ๐ต ) )
5 4 eleq2d โŠข ( ๐‘ฅ = ๐ต โ†’ ( ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฅ ) โ†” ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐ต ) ) )
6 3 5 imbi12d โŠข ( ๐‘ฅ = ๐ต โ†’ ( ( ๐ด โˆˆ ๐‘ฅ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฅ ) ) โ†” ( ๐ด โˆˆ ๐ต โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐ต ) ) ) )
7 6 imbi2d โŠข ( ๐‘ฅ = ๐ต โ†’ ( ( ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โˆง โˆ… โˆˆ ๐ถ ) โ†’ ( ๐ด โˆˆ ๐‘ฅ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฅ ) ) ) โ†” ( ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โˆง โˆ… โˆˆ ๐ถ ) โ†’ ( ๐ด โˆˆ ๐ต โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐ต ) ) ) ) )
8 eleq2 โŠข ( ๐‘ฅ = โˆ… โ†’ ( ๐ด โˆˆ ๐‘ฅ โ†” ๐ด โˆˆ โˆ… ) )
9 oveq2 โŠข ( ๐‘ฅ = โˆ… โ†’ ( ๐ถ ยทo ๐‘ฅ ) = ( ๐ถ ยทo โˆ… ) )
10 9 eleq2d โŠข ( ๐‘ฅ = โˆ… โ†’ ( ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฅ ) โ†” ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo โˆ… ) ) )
11 8 10 imbi12d โŠข ( ๐‘ฅ = โˆ… โ†’ ( ( ๐ด โˆˆ ๐‘ฅ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฅ ) ) โ†” ( ๐ด โˆˆ โˆ… โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo โˆ… ) ) ) )
12 eleq2 โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ๐ด โˆˆ ๐‘ฅ โ†” ๐ด โˆˆ ๐‘ฆ ) )
13 oveq2 โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ๐ถ ยทo ๐‘ฅ ) = ( ๐ถ ยทo ๐‘ฆ ) )
14 13 eleq2d โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฅ ) โ†” ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฆ ) ) )
15 12 14 imbi12d โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ( ๐ด โˆˆ ๐‘ฅ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฅ ) ) โ†” ( ๐ด โˆˆ ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฆ ) ) ) )
16 eleq2 โŠข ( ๐‘ฅ = suc ๐‘ฆ โ†’ ( ๐ด โˆˆ ๐‘ฅ โ†” ๐ด โˆˆ suc ๐‘ฆ ) )
17 oveq2 โŠข ( ๐‘ฅ = suc ๐‘ฆ โ†’ ( ๐ถ ยทo ๐‘ฅ ) = ( ๐ถ ยทo suc ๐‘ฆ ) )
18 17 eleq2d โŠข ( ๐‘ฅ = suc ๐‘ฆ โ†’ ( ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฅ ) โ†” ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo suc ๐‘ฆ ) ) )
19 16 18 imbi12d โŠข ( ๐‘ฅ = suc ๐‘ฆ โ†’ ( ( ๐ด โˆˆ ๐‘ฅ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฅ ) ) โ†” ( ๐ด โˆˆ suc ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo suc ๐‘ฆ ) ) ) )
20 noel โŠข ยฌ ๐ด โˆˆ โˆ…
21 20 pm2.21i โŠข ( ๐ด โˆˆ โˆ… โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo โˆ… ) )
22 21 a1i โŠข ( ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โˆง โˆ… โˆˆ ๐ถ ) โ†’ ( ๐ด โˆˆ โˆ… โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo โˆ… ) ) )
23 elsuci โŠข ( ๐ด โˆˆ suc ๐‘ฆ โ†’ ( ๐ด โˆˆ ๐‘ฆ โˆจ ๐ด = ๐‘ฆ ) )
24 nnmcl โŠข ( ( ๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰ ) โ†’ ( ๐ถ ยทo ๐‘ฆ ) โˆˆ ฯ‰ )
25 simpl โŠข ( ( ๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰ ) โ†’ ๐ถ โˆˆ ฯ‰ )
26 24 25 jca โŠข ( ( ๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰ ) โ†’ ( ( ๐ถ ยทo ๐‘ฆ ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) )
27 nnaword1 โŠข ( ( ( ๐ถ ยทo ๐‘ฆ ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โ†’ ( ๐ถ ยทo ๐‘ฆ ) โŠ† ( ( ๐ถ ยทo ๐‘ฆ ) +o ๐ถ ) )
28 27 sseld โŠข ( ( ( ๐ถ ยทo ๐‘ฆ ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โ†’ ( ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฆ ) โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ( ๐ถ ยทo ๐‘ฆ ) +o ๐ถ ) ) )
29 28 imim2d โŠข ( ( ( ๐ถ ยทo ๐‘ฆ ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โ†’ ( ( ๐ด โˆˆ ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฆ ) ) โ†’ ( ๐ด โˆˆ ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ( ๐ถ ยทo ๐‘ฆ ) +o ๐ถ ) ) ) )
30 29 imp โŠข ( ( ( ( ๐ถ ยทo ๐‘ฆ ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โˆง ( ๐ด โˆˆ ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฆ ) ) ) โ†’ ( ๐ด โˆˆ ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ( ๐ถ ยทo ๐‘ฆ ) +o ๐ถ ) ) )
31 30 adantrl โŠข ( ( ( ( ๐ถ ยทo ๐‘ฆ ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โˆง ( โˆ… โˆˆ ๐ถ โˆง ( ๐ด โˆˆ ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฆ ) ) ) ) โ†’ ( ๐ด โˆˆ ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ( ๐ถ ยทo ๐‘ฆ ) +o ๐ถ ) ) )
32 nna0 โŠข ( ( ๐ถ ยทo ๐‘ฆ ) โˆˆ ฯ‰ โ†’ ( ( ๐ถ ยทo ๐‘ฆ ) +o โˆ… ) = ( ๐ถ ยทo ๐‘ฆ ) )
33 32 ad2antrr โŠข ( ( ( ( ๐ถ ยทo ๐‘ฆ ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โˆง โˆ… โˆˆ ๐ถ ) โ†’ ( ( ๐ถ ยทo ๐‘ฆ ) +o โˆ… ) = ( ๐ถ ยทo ๐‘ฆ ) )
34 nnaordi โŠข ( ( ๐ถ โˆˆ ฯ‰ โˆง ( ๐ถ ยทo ๐‘ฆ ) โˆˆ ฯ‰ ) โ†’ ( โˆ… โˆˆ ๐ถ โ†’ ( ( ๐ถ ยทo ๐‘ฆ ) +o โˆ… ) โˆˆ ( ( ๐ถ ยทo ๐‘ฆ ) +o ๐ถ ) ) )
35 34 ancoms โŠข ( ( ( ๐ถ ยทo ๐‘ฆ ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โ†’ ( โˆ… โˆˆ ๐ถ โ†’ ( ( ๐ถ ยทo ๐‘ฆ ) +o โˆ… ) โˆˆ ( ( ๐ถ ยทo ๐‘ฆ ) +o ๐ถ ) ) )
36 35 imp โŠข ( ( ( ( ๐ถ ยทo ๐‘ฆ ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โˆง โˆ… โˆˆ ๐ถ ) โ†’ ( ( ๐ถ ยทo ๐‘ฆ ) +o โˆ… ) โˆˆ ( ( ๐ถ ยทo ๐‘ฆ ) +o ๐ถ ) )
37 33 36 eqeltrrd โŠข ( ( ( ( ๐ถ ยทo ๐‘ฆ ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โˆง โˆ… โˆˆ ๐ถ ) โ†’ ( ๐ถ ยทo ๐‘ฆ ) โˆˆ ( ( ๐ถ ยทo ๐‘ฆ ) +o ๐ถ ) )
38 oveq2 โŠข ( ๐ด = ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) = ( ๐ถ ยทo ๐‘ฆ ) )
39 38 eleq1d โŠข ( ๐ด = ๐‘ฆ โ†’ ( ( ๐ถ ยทo ๐ด ) โˆˆ ( ( ๐ถ ยทo ๐‘ฆ ) +o ๐ถ ) โ†” ( ๐ถ ยทo ๐‘ฆ ) โˆˆ ( ( ๐ถ ยทo ๐‘ฆ ) +o ๐ถ ) ) )
40 37 39 syl5ibrcom โŠข ( ( ( ( ๐ถ ยทo ๐‘ฆ ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โˆง โˆ… โˆˆ ๐ถ ) โ†’ ( ๐ด = ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ( ๐ถ ยทo ๐‘ฆ ) +o ๐ถ ) ) )
41 40 adantrr โŠข ( ( ( ( ๐ถ ยทo ๐‘ฆ ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โˆง ( โˆ… โˆˆ ๐ถ โˆง ( ๐ด โˆˆ ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฆ ) ) ) ) โ†’ ( ๐ด = ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ( ๐ถ ยทo ๐‘ฆ ) +o ๐ถ ) ) )
42 31 41 jaod โŠข ( ( ( ( ๐ถ ยทo ๐‘ฆ ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โˆง ( โˆ… โˆˆ ๐ถ โˆง ( ๐ด โˆˆ ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฆ ) ) ) ) โ†’ ( ( ๐ด โˆˆ ๐‘ฆ โˆจ ๐ด = ๐‘ฆ ) โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ( ๐ถ ยทo ๐‘ฆ ) +o ๐ถ ) ) )
43 26 42 sylan โŠข ( ( ( ๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰ ) โˆง ( โˆ… โˆˆ ๐ถ โˆง ( ๐ด โˆˆ ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฆ ) ) ) ) โ†’ ( ( ๐ด โˆˆ ๐‘ฆ โˆจ ๐ด = ๐‘ฆ ) โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ( ๐ถ ยทo ๐‘ฆ ) +o ๐ถ ) ) )
44 23 43 syl5 โŠข ( ( ( ๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰ ) โˆง ( โˆ… โˆˆ ๐ถ โˆง ( ๐ด โˆˆ ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฆ ) ) ) ) โ†’ ( ๐ด โˆˆ suc ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ( ๐ถ ยทo ๐‘ฆ ) +o ๐ถ ) ) )
45 nnmsuc โŠข ( ( ๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰ ) โ†’ ( ๐ถ ยทo suc ๐‘ฆ ) = ( ( ๐ถ ยทo ๐‘ฆ ) +o ๐ถ ) )
46 45 eleq2d โŠข ( ( ๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰ ) โ†’ ( ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo suc ๐‘ฆ ) โ†” ( ๐ถ ยทo ๐ด ) โˆˆ ( ( ๐ถ ยทo ๐‘ฆ ) +o ๐ถ ) ) )
47 46 adantr โŠข ( ( ( ๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰ ) โˆง ( โˆ… โˆˆ ๐ถ โˆง ( ๐ด โˆˆ ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฆ ) ) ) ) โ†’ ( ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo suc ๐‘ฆ ) โ†” ( ๐ถ ยทo ๐ด ) โˆˆ ( ( ๐ถ ยทo ๐‘ฆ ) +o ๐ถ ) ) )
48 44 47 sylibrd โŠข ( ( ( ๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰ ) โˆง ( โˆ… โˆˆ ๐ถ โˆง ( ๐ด โˆˆ ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฆ ) ) ) ) โ†’ ( ๐ด โˆˆ suc ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo suc ๐‘ฆ ) ) )
49 48 exp43 โŠข ( ๐ถ โˆˆ ฯ‰ โ†’ ( ๐‘ฆ โˆˆ ฯ‰ โ†’ ( โˆ… โˆˆ ๐ถ โ†’ ( ( ๐ด โˆˆ ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฆ ) ) โ†’ ( ๐ด โˆˆ suc ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo suc ๐‘ฆ ) ) ) ) ) )
50 49 com12 โŠข ( ๐‘ฆ โˆˆ ฯ‰ โ†’ ( ๐ถ โˆˆ ฯ‰ โ†’ ( โˆ… โˆˆ ๐ถ โ†’ ( ( ๐ด โˆˆ ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฆ ) ) โ†’ ( ๐ด โˆˆ suc ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo suc ๐‘ฆ ) ) ) ) ) )
51 50 adantld โŠข ( ๐‘ฆ โˆˆ ฯ‰ โ†’ ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โ†’ ( โˆ… โˆˆ ๐ถ โ†’ ( ( ๐ด โˆˆ ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฆ ) ) โ†’ ( ๐ด โˆˆ suc ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo suc ๐‘ฆ ) ) ) ) ) )
52 51 impd โŠข ( ๐‘ฆ โˆˆ ฯ‰ โ†’ ( ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โˆง โˆ… โˆˆ ๐ถ ) โ†’ ( ( ๐ด โˆˆ ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฆ ) ) โ†’ ( ๐ด โˆˆ suc ๐‘ฆ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo suc ๐‘ฆ ) ) ) ) )
53 11 15 19 22 52 finds2 โŠข ( ๐‘ฅ โˆˆ ฯ‰ โ†’ ( ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โˆง โˆ… โˆˆ ๐ถ ) โ†’ ( ๐ด โˆˆ ๐‘ฅ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐‘ฅ ) ) ) )
54 7 53 vtoclga โŠข ( ๐ต โˆˆ ฯ‰ โ†’ ( ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โˆง โˆ… โˆˆ ๐ถ ) โ†’ ( ๐ด โˆˆ ๐ต โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐ต ) ) ) )
55 54 com23 โŠข ( ๐ต โˆˆ ฯ‰ โ†’ ( ๐ด โˆˆ ๐ต โ†’ ( ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โˆง โˆ… โˆˆ ๐ถ ) โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐ต ) ) ) )
56 55 exp4a โŠข ( ๐ต โˆˆ ฯ‰ โ†’ ( ๐ด โˆˆ ๐ต โ†’ ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โ†’ ( โˆ… โˆˆ ๐ถ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐ต ) ) ) ) )
57 56 exp4a โŠข ( ๐ต โˆˆ ฯ‰ โ†’ ( ๐ด โˆˆ ๐ต โ†’ ( ๐ด โˆˆ ฯ‰ โ†’ ( ๐ถ โˆˆ ฯ‰ โ†’ ( โˆ… โˆˆ ๐ถ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐ต ) ) ) ) ) )
58 2 57 mpdd โŠข ( ๐ต โˆˆ ฯ‰ โ†’ ( ๐ด โˆˆ ๐ต โ†’ ( ๐ถ โˆˆ ฯ‰ โ†’ ( โˆ… โˆˆ ๐ถ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐ต ) ) ) ) )
59 58 com34 โŠข ( ๐ต โˆˆ ฯ‰ โ†’ ( ๐ด โˆˆ ๐ต โ†’ ( โˆ… โˆˆ ๐ถ โ†’ ( ๐ถ โˆˆ ฯ‰ โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐ต ) ) ) ) )
60 59 com24 โŠข ( ๐ต โˆˆ ฯ‰ โ†’ ( ๐ถ โˆˆ ฯ‰ โ†’ ( โˆ… โˆˆ ๐ถ โ†’ ( ๐ด โˆˆ ๐ต โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐ต ) ) ) ) )
61 60 imp31 โŠข ( ( ( ๐ต โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โˆง โˆ… โˆˆ ๐ถ ) โ†’ ( ๐ด โˆˆ ๐ต โ†’ ( ๐ถ ยทo ๐ด ) โˆˆ ( ๐ถ ยทo ๐ต ) ) )